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  1163  3adant1l  1232  reu6  2953  sbc2iegf  3060  sbcralt  3066  sbcrext  3067  indifdir  3420  pofun  4348  poinxp  4733  ssimaex  5625  fndmdif  5670  dffo4  5713  fcompt  5735  fconst2g  5780  foco2  5803  foeqcnvco  5840  f1eqcocnv  5841  fliftel1  5844  isores3  5865  acexmid  5924  tfrlemi14d  6400  tfrcl  6431  dom2lem  6840  fiintim  7001  ordiso2  7110  mkvprop  7233  lt2addnq  7488  lt2mulnq  7489  ltexnqq  7492  genpdf  7592  addnqprl  7613  addnqpru  7614  addlocpr  7620  recexprlemopl  7709  caucvgsrlemgt1  7879  add4  8204  cnegex  8221  ltleadd  8490  zextle  9434  peano5uzti  9451  fnn0ind  9459  xrlttr  9887  xaddass  9961  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  fzaddel  10151  fzrev  10176  exbtwnzlemshrink  10355  xqltnle  10374  seq3val  10569  iseqf1olemab  10611  seqf1og  10630  exp3vallem  10649  mulexp  10687  expadd  10690  expmul  10693  leexp1a  10703  bccl  10876  hashfacen  10945  wrdnval  10982  ovshftex  11001  2shfti  11013  caucvgre  11163  cvg1nlemcau  11166  resqrexlemcvg  11201  cau3lem  11296  rexico  11403  iooinsup  11459  climmpt  11482  subcn2  11493  climrecvg1n  11530  climcvg1nlem  11531  climcaucn  11533  mertenslem2  11718  eftlcl  11870  reeftlcl  11871  dvdsext  12037  3dvds  12046  sqoddm1div8z  12068  bezoutlemaz  12195  bezoutr1  12225  dvdslcm  12262  lcmeq0  12264  lcmcl  12265  lcmneg  12267  lcmdvds  12272  coprmgcdb  12281  dvdsprime  12315  pc2dvds  12524  prmpwdvds  12549  infpnlem1  12553  1arith  12561  resmhm  13189  resmhm2b  13191  mhmco  13192  mhmima  13193  gsumwsubmcl  13198  dfgrp2  13229  mulgfng  13330  subgintm  13404  ghmmhmb  13460  resghm  13466  islmod  13923  islmodd  13925  cnco  14541  cnss1  14546  tx2cn  14590  upxp  14592  metss  14814  txmetcnp  14838  cncfss  14903  plyaddlem1  15067  plymullem1  15068  cosz12  15100  gausslemma2dlem4  15389  bj-findis  15709