Theorem adantll 460

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  ad2antlr  473  ad2ant2l  492  ad2ant2lr  494  3ad2antl3  1105  3adant1l  1164  reu6  2795  sbc2iegf  2898  sbcralt  2904  sbcrext  2905  indifdir  3244  pofun  4115  poinxp  4477  ssimaex  5330  fndmdif  5369  dffo4  5412  fcompt  5432  fconst2g  5475  foco2  5496  foeqcnvco  5532  f1eqcocnv  5533  fliftel1  5536  isores3  5557  acexmid  5614  tfrlemi14d  6054  tfrcl  6085  dom2lem  6443  ordiso2  6675  lt2addnq  6910  lt2mulnq  6911  ltexnqq  6914  genpdf  7014  addnqprl  7035  addnqpru  7036  addlocpr  7042  recexprlemopl  7131  caucvgsrlemgt1  7287  add4  7590  cnegex  7607  ltleadd  7871  zextle  8773  peano5uzti  8790  fnn0ind  8798  xrlttr  9200  iccshftr  9346  iccshftl  9348  iccdil  9350  icccntr  9352  fzaddel  9407  fzrev  9431  exbtwnzlemshrink  9591  iseqvalt  9793  iseqf1olemab  9826  expivallem  9858  expival  9859  mulexp  9896  expadd  9899  expmul  9902  leexp1a  9912  bccl  10075  hashfacen  10141  ovshftex  10153  2shfti  10165  caucvgre  10313  cvg1nlemcau  10316  resqrexlemcvg  10351  cau3lem  10446  rexico  10553  climmpt  10586  subcn2  10597  climrecvg1n  10632  climcvg1nlem  10633  climcaucn  10635  dvdsext  10762  sqoddm1div8z  10792  bezoutlemaz  10898  bezoutr1  10928  dvdslcm  10957  lcmeq0  10959  lcmcl  10960  lcmneg  10962  lcmdvds  10967  coprmgcdb  10976  dvdsprime  11010  bj-findis  11343