Theorem prlem2 577

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

Assertion

Ref	Expression
prlem2	⊢ (((φ ∧ ψ) ∨ (χ ∧ θ)) ↔ ((φ ∨ χ) ∧ ((φ ∧ ψ) ∨ (χ ∧ θ))))

Proof of Theorem prlem2

Step	Hyp	Ref	Expression
1		oel 441	. . . . 5 ⊢ (φ ↔ ((φ ∨ χ) ∧ φ))
2	1	anbi1i 368	. . . 4 ⊢ ((φ ∧ ψ) ↔ (((φ ∨ χ) ∧ φ) ∧ ψ))
3		anass 336	. . . 4 ⊢ ((((φ ∨ χ) ∧ φ) ∧ ψ) ↔ ((φ ∨ χ) ∧ (φ ∧ ψ)))
4	2, 3	bitr 151	. . 3 ⊢ ((φ ∧ ψ) ↔ ((φ ∨ χ) ∧ (φ ∧ ψ)))
5		oel 441	. . . . . 6 ⊢ (χ ↔ ((χ ∨ φ) ∧ χ))
6		orcom 209	. . . . . . 7 ⊢ ((χ ∨ φ) ↔ (φ ∨ χ))
7	6	anbi1i 368	. . . . . 6 ⊢ (((χ ∨ φ) ∧ χ) ↔ ((φ ∨ χ) ∧ χ))
8	5, 7	bitr 151	. . . . 5 ⊢ (χ ↔ ((φ ∨ χ) ∧ χ))
9	8	anbi1i 368	. . . 4 ⊢ ((χ ∧ θ) ↔ (((φ ∨ χ) ∧ χ) ∧ θ))
10		anass 336	. . . 4 ⊢ ((((φ ∨ χ) ∧ χ) ∧ θ) ↔ ((φ ∨ χ) ∧ (χ ∧ θ)))
11	9, 10	bitr 151	. . 3 ⊢ ((χ ∧ θ) ↔ ((φ ∨ χ) ∧ (χ ∧ θ)))
12	4, 11	orbi12i 216	. 2 ⊢ (((φ ∧ ψ) ∨ (χ ∧ θ)) ↔ (((φ ∨ χ) ∧ (φ ∧ ψ)) ∨ ((φ ∨ χ) ∧ (χ ∧ θ))))
13		andi 456	. 2 ⊢ (((φ ∨ χ) ∧ ((φ ∧ ψ) ∨ (χ ∧ θ))) ↔ (((φ ∨ χ) ∧ (φ ∧ ψ)) ∨ ((φ ∨ χ) ∧ (χ ∧ θ))))
14	12, 13	bitr4 154	1 ⊢ (((φ ∧ ψ) ∨ (χ ∧ θ)) ↔ ((φ ∨ χ) ∧ ((φ ∧ ψ) ∨ (χ ∧ θ))))

Syntax hints:   ↔ 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