Theorem ad2antrl 459

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antrl	⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Proof of Theorem ad2antrl

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 261	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantl 262	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  simprl  483  simprll  489  simprlr  490  elxp5  4809  f1oprg  5168  cnvf1olem  5845  nnaordi  6081  swoer  6134  0er  6140  php5fin  6339  fin0  6342  fin0or  6343  diffisn  6350  enq0sym  6530  nqnq0pi  6536  addlocpr  6634  nqprl  6649  addnqprlemrl  6655  addnqprlemru  6656  mulnqprlemrl  6671  mulnqprlemru  6672  archpr  6741  cauappcvgprlemloc  6750  cauappcvgprlemladdfl  6753  archrecpr  6762  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemdisj  6800  caucvgprprlemloc  6801  mulcmpblnrlemg  6825  caucvgsrlemgt1  6879  axarch  6965  axcaucvglemres  6973  cnegexlem2  7187  mulge0  7610  divdivap1  7699  divdivap2  7700  conjmulap  7705  ltdivmul  7842  nn0ge0div  8327  peano2uz2  8345  peano5uzti  8346  eluzp1m1  8496  iooshf  8821  divelunit  8870  eluzgtdifelfzo  9053  iseqval  9220  iseqfveq2  9228  expineg2  9264  mulexpzap  9295  leexp2r  9308  expnlbnd2  9374  resqrexlemp1rp  9604  resqrexlemfp1  9607  climcaucn  9870  qdencn  10124