Theorem ad2antll 460

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

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ad2antll

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 262	. 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:  simprr  484  simprrl  491  simprrr  492  dn1dc  867  prneimg  3545  f1oprg  5168  fidceq  6330  fidifsnen  6331  php5fin  6339  findcard2d  6348  findcard2sd  6349  diffisn  6350  subhalfnqq  6512  nqnq0pi  6536  genprndl  6619  genprndu  6620  addlocpr  6634  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  mullocpr  6669  mulnqprlemrl  6671  mulnqprlemru  6672  ltaprlem  6716  aptiprleml  6737  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemladdfu  6775  caucvgprprlemloc  6801  mulcmpblnrlemg  6825  recexgt0sr  6858  pitonn  6924  rereceu  6963  rimul  7576  receuap  7650  peano5uzti  8346  iooshf  8821  iseqfveq2  9228  expcl2lemap  9267  mulexpzap  9295  expnlbnd2  9374  absexpzap  9676