Metamath Proof Explorer

Theorem prlem1

Description: A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 13-May-2011) (Proof shortened by Wolf Lammen, 5-Jan-2013)

	Ref	Expression
Hypotheses	prlem1.1	$⊢ φ \to (η \leftrightarrow χ)$
	prlem1.2	$⊢ ψ \to \neg θ$
Assertion	prlem1	$⊢ φ \to (ψ \to (((ψ \land χ) \lor (θ \land τ)) \to η))$

Proof

Step	Hyp	Ref	Expression
1		prlem1.1	$⊢ φ \to (η \leftrightarrow χ)$
2		prlem1.2	$⊢ ψ \to \neg θ$
3	1	biimprd	$⊢ φ \to (χ \to η)$
4	3	adantld	$⊢ φ \to ((ψ \land χ) \to η)$
5	2	pm2.21d	$⊢ ψ \to (θ \to η)$
6	5	adantrd	$⊢ ψ \to ((θ \land τ) \to η)$
7	4 6	jaao	$⊢ (φ \land ψ) \to (((ψ \land χ) \lor (θ \land τ)) \to η)$
8	7	ex	$⊢ φ \to (ψ \to (((ψ \land χ) \lor (θ \land τ)) \to η))$