Theorem 3ad2ant1 806

Description: Deduction adding conjuncts to an antecedent.

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (φ → χ)

Assertion

Ref	Expression
3ad2ant1	⊢ ((φ ⋀ ψ ⋀ θ) → χ)

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (φ → χ)
2	1	adantr 389	. 2 ⊢ ((φ ⋀ θ) → χ)
3	2	3adant2 804	1 ⊢ ((φ ⋀ ψ ⋀ θ) → χ)

Syntax hints:   → wi 3   ⋀ w3a 781

This theorem is referenced by:  sbciegft 2007  itlso 2942  reuuniss 3112  onopruni 4210  onopriun 4211  oneo 4348  fodomr 4628  alephval3 5053  ltasr 5363  cnegexlem1 5499  divdiv1 5934  divdiv2 5935  ltmulgt11 5990  lt2mul2divOLD 6017  lediv2 6036  ledivp1i 6051  ltdivp1i 6052  nndivtr 6106  suprleub 6227  supxrun 6253  zdivmul 6358  gtndiv 6364  modcyc 6475  moddi 6479  modsubdir 6480  lbicc2 6531  icoshftf1olem 6537  eluzp1p1 6562  infmssuzle 6592  infmssuzleOLD 6593  eluzfz1 6615  seqzval 6735  seqzval2 6748  seqzcl 6753  expm1 6795  expwordi 6800  expword2i 6802  expubnd 6805  sqlecan 6838  bernneq2 6851  expnlbnd 6853  expnlbnd2 6854  digit2 6855  mulre 6978  fsum1p 7222  fsumshft 7234  serz1p 7255  serzmulc1 7260  iserzgt0 7415  isummulc1 7416  ivthlem6 7491  ivthlem7 7492  sin02gt0 7687  tgtop11 7846  tgss 7848  elcls3 7921  neiint 7929  neips 7937  opnneissb 7938  opnssneib 7939  islp2 7957  iscnp2 7971  cnpco 7979  cnconst 7990  bl2in 8053  metcnpf 8094  metcnp 8098  metidcn 8111  metdnsconst 8112  cncfmet 8116  tgioolem 8125  caussi 8165  iscms2lem4 8203  grpdivval 8300  gxnn0add 8330  gxdi 8355  imsdval 8564  nvelbl 8572  nvcnpf 8575  nvcni 8576  nvcni2 8577  nvlmle 8580  vacnlem3 8584  ipval 8607  lno0 8671  nvcnpi3 8676  nvcnpi4 8677  nmoubi 8689  nmobndi 8692  isblo3i 8716  phpar2 8738  phpar 8739  spwval2 8915  spwpr4c 8928  pilem1 8938  sinq12gt0t 8975  sincosq1eq 8977  efif1lem1 9002  efif1lem2 9003  his52 9230  bcs2 9325  spansncol 9767  pjspansn 9776  nmoplb 10111  nmopub 10112  unop 10119  hmop 10126  nmfnlb 10128  nmfnleub 10129  lnopmul 10170  nmcopexlem5 10234  nmcfnexlem5 10263  leopmul 10347  hstel 10423  ghomid 10679  ghomf1olem 10681  nndivsub 10706  feq123 10774  njtlc 10804  islatalg 10831  cur1val 10846  seqzp2 10918  multinv 10959  multinvb 10960  mult2inv 10961  truni1 10999  truni3 11001  homeofval 11022  hmphsyma 11034  homcard 11045  hmeobc 11048  fipfil2 11077  neifil 11080  filintf 11081  fgsb 11082  cnfilca 11088  rcfpfillem6 11094  bwt2 11123  altretop 11144  mslb1 11152  2wsms 11153  1cat 11213  cmpmorp 11233  icmpmon 11271  iepiclem 11278  idfisf 11295  obsubc2 11304  idsubc 11305  idsubfun 11312  elfiun 11421  ordiso 11426  ordtypelem2 11428  elomsubsd 11446  clsun 11465  hausnei2 11471  cnpnei 11472  compsublem 11487  compsub 11488  cptclsscpt 11489  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem3 11498  alexsublem4 11499  connsub 11502  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  reconnlem3 11509  reconnlem4 11510  reconnlem5 11511  iccconn 11514  ivthALT 11515  2ndc1stc 11538  fness 11552  ssref 11553  fnetr 11556  reftr 11558  topfne 11561  fnessref 11564  islocfin 11567  locfincomp 11575  comppfsc 11578  neibastop1 11579  topmtcl 11586  fnemeet1 11589  ist1-3 11604  opnfbas 11629  fsubbas 11630  fgss 11634  fgfil 11638  fgmin 11639  fbfgss 11640  neifg 11644  supfil 11645  ufprim 11654  filufint 11659  uffinfix 11662  ufinffr 11663  ufilen 11664  limfil 11675  fbaslim 11680  flimcls 11684  hausfillim 11685  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem2 11701  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  isflimf 11709  flimfnei 11710  filclus 11717  isfclus 11718  fclusnei 11719  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscomp 11733  ufcomp 11734  fclusfnei 11738  uffcfflf 11742  isga 11772  gaid 11776  upxp 11822  upixp 11823  fimax 11837  fisupg 11839  fimaxre 11856  sdc 11877  metf1o 11907  mettrifi2 11913  geomcau 11914  iccss 11920  iirev 11935  iihalf1 11936  iihalf2 11937  paste 11954  hmeocnv 11959  tlmbr 11965  lmtlm 11969  2txcn 11982  totbndss 11993  blbnd 11999  ismtybndlem 12008  heiborlem10 12020  heiborlem27 12037  heiborlem28 12038  heiborlem39 12049  rrnmet 12072  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  iccbnd 12082  phtpyval 12089  isphtpc 12101

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223  df-3an 783

Copyright terms: Public domain