This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orim12d

Description: Disjoin antecedents and consequents in a deduction. See orim12dALT for a proof which does not depend on df-an . (Contributed by NM, 10-May-1994)

	Ref	Expression
Hypotheses	orim12d.1	$⊢ φ \to (ψ \to χ)$
	orim12d.2	$⊢ φ \to (θ \to τ)$
Assertion	orim12d	$⊢ φ \to ((ψ \lor θ) \to (χ \lor τ))$

Proof

Step	Hyp	Ref	Expression
1		orim12d.1	$⊢ φ \to (ψ \to χ)$
2		orim12d.2	$⊢ φ \to (θ \to τ)$
3		pm3.48	$⊢ ((ψ \to χ) \land (θ \to τ)) \to ((ψ \lor θ) \to (χ \lor τ))$
4	1 2 3	syl2anc	$⊢ φ \to ((ψ \lor θ) \to (χ \lor τ))$