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  1187  3adant1l  1256  reu6  2995  sbc2iegf  3102  sbcralt  3108  sbcrext  3109  indifdir  3463  pofun  4409  poinxp  4795  ssimaex  5707  fndmdif  5752  dffo4  5795  fcompt  5817  fconst2g  5869  foco2  5894  foeqcnvco  5931  f1eqcocnv  5932  fliftel1  5935  isores3  5956  acexmid  6017  tfrlemi14d  6499  tfrcl  6530  dom2lem  6945  fiintim  7123  ordiso2  7234  mkvprop  7357  lt2addnq  7624  lt2mulnq  7625  ltexnqq  7628  genpdf  7728  addnqprl  7749  addnqpru  7750  addlocpr  7756  recexprlemopl  7845  caucvgsrlemgt1  8015  add4  8340  cnegex  8357  ltleadd  8626  zextle  9571  peano5uzti  9588  fnn0ind  9596  xrlttr  10030  xaddass  10104  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzaddel  10294  fzrev  10319  exbtwnzlemshrink  10509  xqltnle  10528  seq3val  10723  iseqf1olemab  10765  seqf1og  10784  exp3vallem  10803  mulexp  10841  expadd  10844  expmul  10847  leexp1a  10857  bccl  11030  hashfacen  11101  wrdnval  11148  swrdccat3blem  11324  ovshftex  11397  2shfti  11409  caucvgre  11559  cvg1nlemcau  11562  resqrexlemcvg  11597  cau3lem  11692  rexico  11799  iooinsup  11855  climmpt  11878  subcn2  11889  climrecvg1n  11926  climcvg1nlem  11927  climcaucn  11929  mertenslem2  12115  eftlcl  12267  reeftlcl  12268  dvdsext  12434  3dvds  12443  sqoddm1div8z  12465  bezoutlemaz  12592  bezoutr1  12622  dvdslcm  12659  lcmeq0  12661  lcmcl  12662  lcmneg  12664  lcmdvds  12669  coprmgcdb  12678  dvdsprime  12712  pc2dvds  12921  prmpwdvds  12946  infpnlem1  12950  1arith  12958  resmhm  13588  resmhm2b  13590  mhmco  13591  mhmima  13592  gsumwsubmcl  13597  dfgrp2  13628  mulgfng  13729  subgintm  13803  ghmmhmb  13859  resghm  13865  islmod  14324  islmodd  14326  cnco  14964  cnss1  14969  tx2cn  15013  upxp  15015  metss  15237  txmetcnp  15261  cncfss  15326  plyaddlem1  15490  plymullem1  15491  cosz12  15523  gausslemma2dlem4  15812  egrsubgr  16133  bj-findis  16625