Theorem adantll 480

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantll	⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 283	1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2antlr  493  ad2ant2l  512  ad2ant2lr  514  ad5ant23  526  ad5ant24  527  ad5ant25  528  3ad2antl3  1192  3adant1l  1261  reu6  3015  sbc2iegf  3122  sbcralt  3128  sbcrext  3129  indifdir  3487  pofun  4457  poinxp  4844  ssimaex  5764  fndmdif  5814  dffo4  5856  fcompt  5878  fconst2g  5930  foco2  5959  foeqcnvco  5996  f1eqcocnv  5997  fliftel1  6000  isores3  6021  acexmid  6084  suppssdc  6500  tfrlemi14d  6604  tfrcl  6635  mapsnd  6970  dom2lem  7058  fiintim  7238  ordiso2  7375  mkvprop  7498  lt2addnq  7771  lt2mulnq  7772  ltexnqq  7775  genpdf  7875  addnqprl  7896  addnqpru  7897  addlocpr  7903  recexprlemopl  7992  caucvgsrlemgt1  8162  add4  8487  cnegex  8504  ltleadd  8774  zextle  9737  peano5uzti  9754  fnn0ind  9762  xrlttr  10197  xaddass  10271  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  fzaddel  10465  fzrev  10491  exbtwnzlemshrink  10683  xqltnle  10702  seq3val  10897  iseqf1olemab  10939  seqf1og  10958  exp3vallem  10977  mulexp  11015  expadd  11018  expmul  11021  leexp1a  11031  bccl  11205  hashfacen  11284  wrdnval  11335  swrdccat3blem  11511  ovshftex  11584  2shfti  11596  caucvgre  11747  cvg1nlemcau  11750  resqrexlemcvg  11785  cau3lem  11880  rexico  11987  iooinsup  12043  climmpt  12066  subcn2  12077  climrecvg1n  12114  climcvg1nlem  12115  climcaucn  12117  mertenslem2  12303  eftlcl  12455  reeftlcl  12456  dvdsext  12622  3dvds  12631  sqoddm1div8z  12653  bezoutlemaz  12780  bezoutr1  12810  dvdslcm  12847  lcmeq0  12849  lcmcl  12850  lcmneg  12852  lcmdvds  12857  coprmgcdb  12866  dvdsprime  12900  pc2dvds  13109  prmpwdvds  13134  infpnlem1  13138  1arith  13146  resmhm  13794  resmhm2b  13796  mhmco  13797  mhmima  13798  gzsumwsubmcl  13801  dfgrp2  13832  mulgfng  13927  subgintm  14001  ghmmhmb  14057  resghm  14063  islmod  14627  islmodd  14629  cnco  15322  cnss1  15327  tx2cn  15371  upxp  15373  metss  15595  txmetcnp  15619  cncfss  15684  plyaddlem1  15848  plymullem1  15849  cosz12  15881  gausslemma2dlem4  16183  egrsubgr  16504  bj-findis  17005