Metamath Proof Explorer


Theorem pm5.75

Description: Theorem *5.75 of WhiteheadRussell p. 126. (Contributed by NM, 3-Jan-2005) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 23-Dec-2012) (Proof shortened by Kyle Wyonch, 12-Feb-2021)

Ref Expression
Assertion pm5.75 χ¬ψφψχφ¬ψχ

Proof

Step Hyp Ref Expression
1 anbi1 φψχφ¬ψψχ¬ψ
2 biorf ¬ψχψχ
3 2 bicomd ¬ψψχχ
4 3 pm5.32ri ψχ¬ψχ¬ψ
5 1 4 bitrdi φψχφ¬ψχ¬ψ
6 abai χ¬ψχχ¬ψ
7 6 rbaib χ¬ψχ¬ψχ
8 5 7 sylan9bbr χ¬ψφψχφ¬ψχ