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

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