Theorem pm2.21ddALT

Description: Alternate proof of pm2.21dd . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pm2.21ddALT.1	$$⊢\phi \to \psi$$
	pm2.21ddALT.2	$$⊢\phi \to \neg \psi$$
Assertion	pm2.21ddALT	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.21ddALT.1	$$⊢\phi \to \psi$$
2		pm2.21ddALT.2	$$⊢\phi \to \neg \psi$$
3	2	pm2.21d	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	1 3	mpd	$$⊢\phi \to \chi$$