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	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜒 ) )
	prlem1.2	⊢ ( 𝜓 → ¬ 𝜃 )
Assertion	prlem1	⊢ ( 𝜑 → ( 𝜓 → ( ( ( 𝜓 ∧ 𝜒 ) ∨ ( 𝜃 ∧ 𝜏 ) ) → 𝜂 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prlem1.1	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜒 ) )
2		prlem1.2	⊢ ( 𝜓 → ¬ 𝜃 )
3	1	biimprd	⊢ ( 𝜑 → ( 𝜒 → 𝜂 ) )
4	3	adantld	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜂 ) )
5	2	pm2.21d	⊢ ( 𝜓 → ( 𝜃 → 𝜂 ) )
6	5	adantrd	⊢ ( 𝜓 → ( ( 𝜃 ∧ 𝜏 ) → 𝜂 ) )
7	4 6	jaao	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝜓 ∧ 𝜒 ) ∨ ( 𝜃 ∧ 𝜏 ) ) → 𝜂 ) )
8	7	ex	⊢ ( 𝜑 → ( 𝜓 → ( ( ( 𝜓 ∧ 𝜒 ) ∨ ( 𝜃 ∧ 𝜏 ) ) → 𝜂 ) ) )