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  866  prneimg  3536  f1oprg  5111  subhalfnqq  6397  nqnq0pi  6421  genprndl  6504  genprndu  6505  addlocpr  6519  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  mullocpr  6552  ltaprlem  6591  aptiprleml  6611  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemladdfu  6648  mulcmpblnrlemg  6668  recexgt0sr  6701  pitonn  6744  rimul  7369  receuap  7432  peano5uzti  8122  iooshf  8591  iseqfveq2  8905  expcl2lemap  8921  mulexpzap  8949  expnlbnd2  9027