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 ) )