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

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 
|- ( ( ( ch -> -. ps ) /\ ( ph <-> ( ps \/ ch ) ) ) -> ( ( ph /\ -. ps ) <-> ch ) )

Proof

Step Hyp Ref Expression
1 anbi1 
 |-  ( ( ph <-> ( ps \/ ch ) ) -> ( ( ph /\ -. ps ) <-> ( ( ps \/ ch ) /\ -. ps ) ) )
2 biorf 
 |-  ( -. ps -> ( ch <-> ( ps \/ ch ) ) )
3 2 bicomd 
 |-  ( -. ps -> ( ( ps \/ ch ) <-> ch ) )
4 3 pm5.32ri 
 |-  ( ( ( ps \/ ch ) /\ -. ps ) <-> ( ch /\ -. ps ) )
5 1 4 bitrdi 
 |-  ( ( ph <-> ( ps \/ ch ) ) -> ( ( ph /\ -. ps ) <-> ( ch /\ -. ps ) ) )
6 abai 
 |-  ( ( ch /\ -. ps ) <-> ( ch /\ ( ch -> -. ps ) ) )
7 6 rbaib 
 |-  ( ( ch -> -. ps ) -> ( ( ch /\ -. ps ) <-> ch ) )
8 5 7 sylan9bbr 
 |-  ( ( ( ch -> -. ps ) /\ ( ph <-> ( ps \/ ch ) ) ) -> ( ( ph /\ -. ps ) <-> ch ) )