Metamath Proof Explorer


Theorem pm5.55

Description: Theorem *5.55 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 20-Jan-2013)

Ref Expression
Assertion pm5.55 ( ( ( 𝜑𝜓 ) ↔ 𝜑 ) ∨ ( ( 𝜑𝜓 ) ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 biort ( 𝜑 → ( 𝜑 ↔ ( 𝜑𝜓 ) ) )
2 1 bicomd ( 𝜑 → ( ( 𝜑𝜓 ) ↔ 𝜑 ) )
3 biorf ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
4 3 bicomd ( ¬ 𝜑 → ( ( 𝜑𝜓 ) ↔ 𝜓 ) )
5 2 4 nsyl5 ( ¬ ( ( 𝜑𝜓 ) ↔ 𝜑 ) → ( ( 𝜑𝜓 ) ↔ 𝜓 ) )
6 5 orri ( ( ( 𝜑𝜓 ) ↔ 𝜑 ) ∨ ( ( 𝜑𝜓 ) ↔ 𝜓 ) )