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

Metamath Proof Explorer

Theorem oplem1

Description: A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995) (Proof shortened by Wolf Lammen, 8-Dec-2012)

		Ref	Expression
	Hypotheses	oplem1.1	$⊢ φ \to (ψ \lor χ)$
		oplem1.2	$⊢ φ \to (θ \lor τ)$
		oplem1.3	$⊢ ψ \leftrightarrow θ$
		oplem1.4	$⊢ χ \to (θ \leftrightarrow τ)$
	Assertion	oplem1	$⊢ φ \to ψ$

Proof

Step	Hyp	Ref	Expression
1		oplem1.1	$⊢ φ \to (ψ \lor χ)$
2		oplem1.2	$⊢ φ \to (θ \lor τ)$
3		oplem1.3	$⊢ ψ \leftrightarrow θ$
4		oplem1.4	$⊢ χ \to (θ \leftrightarrow τ)$
5	3	notbii	$⊢ \neg ψ \leftrightarrow \neg θ$
6	1	ord	$⊢ φ \to (\neg ψ \to χ)$
7	5 6	biimtrrid	$⊢ φ \to (\neg θ \to χ)$
8	2	ord	$⊢ φ \to (\neg θ \to τ)$
9	7 8	jcad	$⊢ φ \to (\neg θ \to (χ \land τ))$
10	4	biimpar	$⊢ (χ \land τ) \to θ$
11	9 10	syl6	$⊢ φ \to (\neg θ \to θ)$
12	11	pm2.18d	$⊢ φ \to θ$
13	12 3	sylibr	$⊢ φ \to ψ$