Theorem pm5.53

Description: Theorem *5.53 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)

	Ref	Expression
Assertion	pm5.53	⊢ ( ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) → 𝜃 ) ↔ ( ( ( 𝜑 → 𝜃 ) ∧ ( 𝜓 → 𝜃 ) ) ∧ ( 𝜒 → 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		jaob	⊢ ( ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) → 𝜃 ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → 𝜃 ) ) )
2		jaob	⊢ ( ( ( 𝜑 ∨ 𝜓 ) → 𝜃 ) ↔ ( ( 𝜑 → 𝜃 ) ∧ ( 𝜓 → 𝜃 ) ) )
3	2	anbi1i	⊢ ( ( ( ( 𝜑 ∨ 𝜓 ) → 𝜃 ) ∧ ( 𝜒 → 𝜃 ) ) ↔ ( ( ( 𝜑 → 𝜃 ) ∧ ( 𝜓 → 𝜃 ) ) ∧ ( 𝜒 → 𝜃 ) ) )
4	1 3	bitri	⊢ ( ( ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) → 𝜃 ) ↔ ( ( ( 𝜑 → 𝜃 ) ∧ ( 𝜓 → 𝜃 ) ) ∧ ( 𝜒 → 𝜃 ) ) )