Theorem pm5.75 821

Description: Theorem *5.75 of [WhiteheadRussell] p. 126. (The proof was shortened by Andrew Salmon, 7-May-2011.)

Assertion

Ref	Expression
pm5.75	|- (((ch -> -. ps) /\ (ph <-> (ps \/ ch))) -> ((ph /\ -. ps) <-> ch))

Proof of Theorem pm5.75

Step	Hyp	Ref	Expression
1		bi1 165	. . . 4 |- ((ph <-> (ps \/ ch)) -> (ph -> (ps \/ ch)))
2		pm5.6 752	. . . 4 |- (((ph /\ -. ps) -> ch) <-> (ph -> (ps \/ ch)))
3	1, 2	sylibr 217	. . 3 |- ((ph <-> (ps \/ ch)) -> ((ph /\ -. ps) -> ch))
4	3	adantl 424	. 2 |- (((ch -> -. ps) /\ (ph <-> (ps \/ ch))) -> ((ph /\ -. ps) -> ch))
5		bi2 166	. . . . . . 7 |- ((ph <-> (ps \/ ch)) -> ((ps \/ ch) -> ph))
6		simpl 346	. . . . . . . 8 |- ((ch /\ -. ps) -> ch)
7	6	olcd 295	. . . . . . 7 |- ((ch /\ -. ps) -> (ps \/ ch))
8	5, 7	syl5 20	. . . . . 6 |- ((ph <-> (ps \/ ch)) -> ((ch /\ -. ps) -> ph))
9	8	exp3a 405	. . . . 5 |- ((ph <-> (ps \/ ch)) -> (ch -> (-. ps -> ph)))
10	9	a2d 16	. . . 4 |- ((ph <-> (ps \/ ch)) -> ((ch -> -. ps) -> (ch -> ph)))
11	10	impcom 378	. . 3 |- (((ch -> -. ps) /\ (ph <-> (ps \/ ch))) -> (ch -> ph))
12		simpl 346	. . 3 |- (((ch -> -. ps) /\ (ph <-> (ps \/ ch))) -> (ch -> -. ps))
13	11, 12	jcad 661	. 2 |- (((ch -> -. ps) /\ (ph <-> (ps \/ ch))) -> (ch -> (ph /\ -. ps)))
14	4, 13	impbid 574	1 |- (((ch -> -. ps) /\ (ph <-> (ps \/ ch))) -> ((ph /\ -. ps) <-> ch))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242

Copyright terms: Public domain