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

Metamath Proof Explorer

Theorem pm5.71

Description: Theorem *5.71 of WhiteheadRussell p. 125. (Contributed by Roy F. Longton, 23-Jun-2005)

		Ref	Expression
	Assertion	pm5.71	⊢ ( ( 𝜓 → ¬ 𝜒 ) → ( ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ↔ ( 𝜑 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		orel2	⊢ ( ¬ 𝜓 → ( ( 𝜑 ∨ 𝜓 ) → 𝜑 ) )
2		orc	⊢ ( 𝜑 → ( 𝜑 ∨ 𝜓 ) )
3	1 2	impbid1	⊢ ( ¬ 𝜓 → ( ( 𝜑 ∨ 𝜓 ) ↔ 𝜑 ) )
4	3	anbi1d	⊢ ( ¬ 𝜓 → ( ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ↔ ( 𝜑 ∧ 𝜒 ) ) )
5		pm2.21	⊢ ( ¬ 𝜒 → ( 𝜒 → ( ( 𝜑 ∨ 𝜓 ) ↔ 𝜑 ) ) )
6	5	pm5.32rd	⊢ ( ¬ 𝜒 → ( ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ↔ ( 𝜑 ∧ 𝜒 ) ) )
7	4 6	ja	⊢ ( ( 𝜓 → ¬ 𝜒 ) → ( ( ( 𝜑 ∨ 𝜓 ) ∧ 𝜒 ) ↔ ( 𝜑 ∧ 𝜒 ) ) )