Theorem a2d 23

Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)

Hypothesis

Ref	Expression
a2d.1	⊢ (φ → (ψ → (χ → θ)))

Assertion

Ref	Expression
a2d	⊢ (φ → ((ψ → χ) → (ψ → θ)))

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 ⊢ (φ → (ψ → (χ → θ)))
2		ax-2 6	. 2 ⊢ ((ψ → (χ → θ)) → ((ψ → χ) → (ψ → θ)))
3	1, 2	syl 14	1 ⊢ (φ → ((ψ → χ) → (ψ → θ)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  mpdd  36  imim2d  48  imim3i  55  loowoz  96  cbv1  1614  ralimdaa  2364  reuss2  3194  finds2  4251  ssrel  4355  ssrel2  4357  ssrelrel  4367  funfvima2  5316  tfrlem1  5845  tfrlemi1  5867  tfri3  5875  rdgon  5893