Theorem adantll 476

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 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad2antlr  489  ad2ant2l  508  ad2ant2lr  510  ad5ant23  522  ad5ant24  523  ad5ant25  524  3ad2antl3  1188  3adant1l  1257  reu6  2996  sbc2iegf  3103  sbcralt  3109  sbcrext  3110  indifdir  3465  pofun  4415  poinxp  4801  ssimaex  5716  fndmdif  5761  dffo4  5803  fcompt  5825  fconst2g  5877  foco2  5904  foeqcnvco  5941  f1eqcocnv  5942  fliftel1  5945  isores3  5966  acexmid  6027  suppssdc  6438  tfrlemi14d  6542  tfrcl  6573  dom2lem  6988  fiintim  7166  ordiso2  7277  mkvprop  7400  lt2addnq  7667  lt2mulnq  7668  ltexnqq  7671  genpdf  7771  addnqprl  7792  addnqpru  7793  addlocpr  7799  recexprlemopl  7888  caucvgsrlemgt1  8058  add4  8382  cnegex  8399  ltleadd  8668  zextle  9615  peano5uzti  9632  fnn0ind  9640  xrlttr  10074  xaddass  10148  iccshftr  10273  iccshftl  10275  iccdil  10277  icccntr  10279  fzaddel  10339  fzrev  10364  exbtwnzlemshrink  10554  xqltnle  10573  seq3val  10768  iseqf1olemab  10810  seqf1og  10829  exp3vallem  10848  mulexp  10886  expadd  10889  expmul  10892  leexp1a  10902  bccl  11075  hashfacen  11146  wrdnval  11193  swrdccat3blem  11369  ovshftex  11442  2shfti  11454  caucvgre  11604  cvg1nlemcau  11607  resqrexlemcvg  11642  cau3lem  11737  rexico  11844  iooinsup  11900  climmpt  11923  subcn2  11934  climrecvg1n  11971  climcvg1nlem  11972  climcaucn  11974  mertenslem2  12160  eftlcl  12312  reeftlcl  12313  dvdsext  12479  3dvds  12488  sqoddm1div8z  12510  bezoutlemaz  12637  bezoutr1  12667  dvdslcm  12704  lcmeq0  12706  lcmcl  12707  lcmneg  12709  lcmdvds  12714  coprmgcdb  12723  dvdsprime  12757  pc2dvds  12966  prmpwdvds  12991  infpnlem1  12995  1arith  13003  resmhm  13633  resmhm2b  13635  mhmco  13636  mhmima  13637  gsumwsubmcl  13642  dfgrp2  13673  mulgfng  13774  subgintm  13848  ghmmhmb  13904  resghm  13910  islmod  14370  islmodd  14372  cnco  15015  cnss1  15020  tx2cn  15064  upxp  15066  metss  15288  txmetcnp  15312  cncfss  15377  plyaddlem1  15541  plymullem1  15542  cosz12  15574  gausslemma2dlem4  15866  egrsubgr  16187  bj-findis  16678