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  1103  3adant1l  1162  reu6  2792  sbc2iegf  2895  sbcralt  2901  sbcrext  2902  indifdir  3238  pofun  4103  poinxp  4465  ssimaex  5310  fndmdif  5349  dffo4  5392  fcompt  5409  fconst2g  5452  foco2  5473  foeqcnvco  5509  f1eqcocnv  5510  fliftel1  5513  isores3  5534  acexmid  5590  tfrlemi14d  6030  tfrcl  6061  dom2lem  6419  ordiso2  6635  lt2addnq  6866  lt2mulnq  6867  ltexnqq  6870  genpdf  6970  addnqprl  6991  addnqpru  6992  addlocpr  6998  recexprlemopl  7087  caucvgsrlemgt1  7243  add4  7546  cnegex  7563  ltleadd  7827  zextle  8733  peano5uzti  8750  fnn0ind  8758  xrlttr  9160  iccshftr  9306  iccshftl  9308  iccdil  9310  icccntr  9312  fzaddel  9367  fzrev  9391  exbtwnzlemshrink  9549  iseqvalt  9751  expivallem  9793  expival  9794  mulexp  9831  expadd  9834  expmul  9837  leexp1a  9847  bccl  10010  hashfacen  10075  ovshftex  10081  2shfti  10093  caucvgre  10241  cvg1nlemcau  10244  resqrexlemcvg  10279  cau3lem  10374  rexico  10481  climmpt  10513  subcn2  10524  climrecvg1n  10559  climcvg1nlem  10560  climcaucn  10562  dvdsext  10636  sqoddm1div8z  10666  bezoutlemaz  10772  bezoutr1  10802  dvdslcm  10831  lcmeq0  10833  lcmcl  10834  lcmneg  10836  lcmdvds  10841  coprmgcdb  10850  dvdsprime  10884  bj-findis  11217