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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used 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  4457  poinxp  4844  ssimaex  5764  fndmdif  5814  dffo4  5856  fcompt  5878  fconst2g  5930  foco2  5959  foeqcnvco  5996  f1eqcocnv  5997  fliftel1  6000  isores3  6021  acexmid  6084  suppssdc  6500  tfrlemi14d  6604  tfrcl  6635  mapsnd  6970  dom2lem  7058  fiintim  7238  ordiso2  7375  mkvprop  7498  lt2addnq  7771  lt2mulnq  7772  ltexnqq  7775  genpdf  7875  addnqprl  7896  addnqpru  7897  addlocpr  7903  recexprlemopl  7992  caucvgsrlemgt1  8162  add4  8488  cnegex  8505  ltleadd  8775  zextle  9741  peano5uzti  9758  fnn0ind  9766  xrlttr  10207  xaddass  10281  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  fzaddel  10475  fzrev  10501  exbtwnzlemshrink  10693  xqltnle  10712  seq3val  10910  iseqf1olemab  10952  seqf1og  10971  exp3vallem  10990  mulexp  11028  expadd  11031  expmul  11034  leexp1a  11044  bccl  11219  hashfacen  11298  wrdnval  11349  swrdccat3blem  11525  ovshftex  11598  2shfti  11610  caucvgre  11761  cvg1nlemcau  11764  resqrexlemcvg  11799  cau3lem  11895  rexico  12002  iooinsup  12059  climmpt  12082  subcn2  12093  climrecvg1n  12130  climcvg1nlem  12131  climcaucn  12133  mertenslem2  12319  eftlcl  12471  reeftlcl  12472  dvdsext  12638  3dvds  12647  sqoddm1div8z  12669  bezoutlemaz  12796  bezoutr1  12826  dvdslcm  12863  lcmeq0  12865  lcmcl  12866  lcmneg  12868  lcmdvds  12873  coprmgcdb  12882  dvdsprime  12916  pc2dvds  13129  prmpwdvds  13154  infpnlem1  13158  1arith  13166  resmhm  13843  resmhm2b  13845  mhmco  13846  mhmima  13847  gzsumwsubmcl  13850  dfgrp2  13881  mulgfng  13976  subgintm  14050  ghmmhmb  14106  resghm  14112  islmod  14676  islmodd  14678  cnco  15371  cnss1  15376  tx2cn  15420  upxp  15422  metss  15644  txmetcnp  15668  cncfss  15733  plyaddlem1  15897  plymullem1  15898  cosz12  15931  bposlem3  16211  gausslemma2dlem4  16281  egrsubgr  16602  bj-findis  17103