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  6420  genprndl  6503  genprndu  6504  addlocpr  6518  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  mullocpr  6551  ltaprlem  6590  aptiprleml  6610  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  mulcmpblnrlemg  6648  recexgt0sr  6681  pitonn  6724  rimul  7349  receuap  7412  peano5uzti  8102  iooshf  8571  iseqfveq2  8885  expcl2lemap  8901  mulexpzap  8929  expnlbnd2  9007