Theorem prlem1 576

Description: A specialized lemma for set theory (axiom of pairing).

Hypotheses

Ref	Expression
prlem1.1	⊢ (φ → (η ↔ χ))
prlem1.2	⊢ (ψ → ¬ θ)

Assertion

Ref	Expression
prlem1	⊢ (φ → (ψ → (((ψ ∧ χ) ∨ (θ ∧ τ)) → η)))

Proof of Theorem prlem1

Step	Hyp	Ref	Expression
1		prlem1.1	. . . . . 6 ⊢ (φ → (η ↔ χ))
2	1	biimprcd 138	. . . . 5 ⊢ (χ → (φ → η))
3	2	adantl 305	. . . 4 ⊢ ((ψ ∧ χ) → (φ → η))
4	3	a1dd 42	. . 3 ⊢ ((ψ ∧ χ) → (φ → (ψ → η)))
5		pm2.24 72	. . . . . 6 ⊢ (θ → (¬ θ → η))
6		prlem1.2	. . . . . 6 ⊢ (ψ → ¬ θ)
7	5, 6	syl5 22	. . . . 5 ⊢ (θ → (ψ → η))
8	7	adantr 306	. . . 4 ⊢ ((θ ∧ τ) → (ψ → η))
9	8	a1d 14	. . 3 ⊢ ((θ ∧ τ) → (φ → (ψ → η)))
10	4, 9	jaoi 275	. 2 ⊢ (((ψ ∧ χ) ∨ (θ ∧ τ)) → (φ → (ψ → η)))
11	10	com3l 34	1 ⊢ (φ → (ψ → (((ψ ∧ χ) ∨ (θ ∧ τ)) → η)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  zfpair 1891

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org