Theorem adantll 467

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 109	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 281	1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2antlr  480  ad2ant2l  499  ad2ant2lr  501  ad5ant23  513  ad5ant24  514  ad5ant25  515  3ad2antl3  1145  3adant1l  1208  reu6  2873  sbc2iegf  2979  sbcralt  2985  sbcrext  2986  indifdir  3332  pofun  4234  poinxp  4608  ssimaex  5482  fndmdif  5525  dffo4  5568  fcompt  5590  fconst2g  5635  foco2  5655  foeqcnvco  5691  f1eqcocnv  5692  fliftel1  5695  isores3  5716  acexmid  5773  tfrlemi14d  6230  tfrcl  6261  dom2lem  6666  fiintim  6817  ordiso2  6920  mkvprop  7032  lt2addnq  7212  lt2mulnq  7213  ltexnqq  7216  genpdf  7316  addnqprl  7337  addnqpru  7338  addlocpr  7344  recexprlemopl  7433  caucvgsrlemgt1  7603  add4  7923  cnegex  7940  ltleadd  8208  zextle  9142  peano5uzti  9159  fnn0ind  9167  xrlttr  9581  xaddass  9652  iccshftr  9777  iccshftl  9779  iccdil  9781  icccntr  9783  fzaddel  9839  fzrev  9864  exbtwnzlemshrink  10026  seq3val  10231  iseqf1olemab  10262  exp3vallem  10294  mulexp  10332  expadd  10335  expmul  10338  leexp1a  10348  bccl  10513  hashfacen  10579  ovshftex  10591  2shfti  10603  caucvgre  10753  cvg1nlemcau  10756  resqrexlemcvg  10791  cau3lem  10886  rexico  10993  iooinsup  11046  climmpt  11069  subcn2  11080  climrecvg1n  11117  climcvg1nlem  11118  climcaucn  11120  mertenslem2  11305  eftlcl  11394  reeftlcl  11395  dvdsext  11553  sqoddm1div8z  11583  bezoutlemaz  11691  bezoutr1  11721  dvdslcm  11750  lcmeq0  11752  lcmcl  11753  lcmneg  11755  lcmdvds  11760  coprmgcdb  11769  dvdsprime  11803  cnco  12390  cnss1  12395  tx2cn  12439  upxp  12441  metss  12663  txmetcnp  12687  cncfss  12739  cosz12  12861  bj-findis  13177