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

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  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  4452  poinxp  4839  ssimaex  5758  fndmdif  5805  dffo4  5847  fcompt  5869  fconst2g  5921  foco2  5949  foeqcnvco  5986  f1eqcocnv  5987  fliftel1  5990  isores3  6011  acexmid  6074  suppssdc  6490  tfrlemi14d  6594  tfrcl  6625  mapsnd  6960  dom2lem  7048  fiintim  7228  ordiso2  7365  mkvprop  7488  lt2addnq  7761  lt2mulnq  7762  ltexnqq  7765  genpdf  7865  addnqprl  7886  addnqpru  7887  addlocpr  7893  recexprlemopl  7982  caucvgsrlemgt1  8152  add4  8477  cnegex  8494  ltleadd  8764  zextle  9716  peano5uzti  9733  fnn0ind  9741  xrlttr  10176  xaddass  10250  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  fzaddel  10443  fzrev  10469  exbtwnzlemshrink  10661  xqltnle  10680  seq3val  10875  iseqf1olemab  10917  seqf1og  10936  exp3vallem  10955  mulexp  10993  expadd  10996  expmul  10999  leexp1a  11009  bccl  11183  hashfacen  11262  wrdnval  11313  swrdccat3blem  11489  ovshftex  11562  2shfti  11574  caucvgre  11725  cvg1nlemcau  11728  resqrexlemcvg  11763  cau3lem  11858  rexico  11965  iooinsup  12021  climmpt  12044  subcn2  12055  climrecvg1n  12092  climcvg1nlem  12093  climcaucn  12095  mertenslem2  12281  eftlcl  12433  reeftlcl  12434  dvdsext  12600  3dvds  12609  sqoddm1div8z  12631  bezoutlemaz  12758  bezoutr1  12788  dvdslcm  12825  lcmeq0  12827  lcmcl  12828  lcmneg  12830  lcmdvds  12835  coprmgcdb  12844  dvdsprime  12878  pc2dvds  13087  prmpwdvds  13112  infpnlem1  13116  1arith  13124  resmhm  13771  resmhm2b  13773  mhmco  13774  mhmima  13775  gzsumwsubmcl  13778  dfgrp2  13809  mulgfng  13904  subgintm  13978  ghmmhmb  14034  resghm  14040  islmod  14600  islmodd  14602  cnco  15245  cnss1  15250  tx2cn  15294  upxp  15296  metss  15518  txmetcnp  15542  cncfss  15607  plyaddlem1  15771  plymullem1  15772  cosz12  15804  gausslemma2dlem4  16097  egrsubgr  16418  bj-findis  16919