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

Metamath Proof Explorer

Theorem pm5.7

Description: Disjunction distributes over the biconditional. Theorem *5.7 of WhiteheadRussell p. 125. This theorem is similar to orbidi . (Contributed by Roy F. Longton, 21-Jun-2005)

		Ref	Expression
	Assertion	pm5.7	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜒 ∨ ( 𝜑 ↔ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		orbidi	⊢ ( ( 𝜒 ∨ ( 𝜑 ↔ 𝜓 ) ) ↔ ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜒 ∨ 𝜓 ) ) )
2		orcom	⊢ ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜑 ∨ 𝜒 ) )
3		orcom	⊢ ( ( 𝜒 ∨ 𝜓 ) ↔ ( 𝜓 ∨ 𝜒 ) )
4	2 3	bibi12i	⊢ ( ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜒 ∨ 𝜓 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) ) )
5	1 4	bitr2i	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜒 ∨ ( 𝜑 ↔ 𝜓 ) ) )