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  1164  3adant1l  1233  reu6  2966  sbc2iegf  3073  sbcralt  3079  sbcrext  3080  indifdir  3433  pofun  4366  poinxp  4751  ssimaex  5652  fndmdif  5697  dffo4  5740  fcompt  5762  fconst2g  5811  foco2  5834  foeqcnvco  5871  f1eqcocnv  5872  fliftel1  5875  isores3  5896  acexmid  5955  tfrlemi14d  6431  tfrcl  6462  dom2lem  6875  fiintim  7042  ordiso2  7151  mkvprop  7274  lt2addnq  7532  lt2mulnq  7533  ltexnqq  7536  genpdf  7636  addnqprl  7657  addnqpru  7658  addlocpr  7664  recexprlemopl  7753  caucvgsrlemgt1  7923  add4  8248  cnegex  8265  ltleadd  8534  zextle  9479  peano5uzti  9496  fnn0ind  9504  xrlttr  9932  xaddass  10006  iccshftr  10131  iccshftl  10133  iccdil  10135  icccntr  10137  fzaddel  10196  fzrev  10221  exbtwnzlemshrink  10408  xqltnle  10427  seq3val  10622  iseqf1olemab  10664  seqf1og  10683  exp3vallem  10702  mulexp  10740  expadd  10743  expmul  10746  leexp1a  10756  bccl  10929  hashfacen  10998  wrdnval  11041  ovshftex  11200  2shfti  11212  caucvgre  11362  cvg1nlemcau  11365  resqrexlemcvg  11400  cau3lem  11495  rexico  11602  iooinsup  11658  climmpt  11681  subcn2  11692  climrecvg1n  11729  climcvg1nlem  11730  climcaucn  11732  mertenslem2  11917  eftlcl  12069  reeftlcl  12070  dvdsext  12236  3dvds  12245  sqoddm1div8z  12267  bezoutlemaz  12394  bezoutr1  12424  dvdslcm  12461  lcmeq0  12463  lcmcl  12464  lcmneg  12466  lcmdvds  12471  coprmgcdb  12480  dvdsprime  12514  pc2dvds  12723  prmpwdvds  12748  infpnlem1  12752  1arith  12760  resmhm  13389  resmhm2b  13391  mhmco  13392  mhmima  13393  gsumwsubmcl  13398  dfgrp2  13429  mulgfng  13530  subgintm  13604  ghmmhmb  13660  resghm  13666  islmod  14123  islmodd  14125  cnco  14763  cnss1  14768  tx2cn  14812  upxp  14814  metss  15036  txmetcnp  15060  cncfss  15125  plyaddlem1  15289  plymullem1  15290  cosz12  15322  gausslemma2dlem4  15611  bj-findis  16049