Metamath Proof Explorer


Theorem pm5.17

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

Ref Expression
Assertion pm5.17 φψ¬φψφ¬ψ

Proof

Step Hyp Ref Expression
1 bicom φ¬ψ¬ψφ
2 dfbi2 ¬ψφ¬ψφφ¬ψ
3 orcom φψψφ
4 df-or ψφ¬ψφ
5 3 4 bitr2i ¬ψφφψ
6 imnan φ¬ψ¬φψ
7 5 6 anbi12i ¬ψφφ¬ψφψ¬φψ
8 1 2 7 3bitrri φψ¬φψφ¬ψ