Theorem pm4.55dc 845

Description: Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.)

Assertion

Ref	Expression
pm4.55dc	|- (DECID ph -> (DECID ps -> (-. (-. ph /\ ps) <-> (ph \/ -. ps))))

Proof of Theorem pm4.55dc

Step	Hyp	Ref	Expression
1		pm4.54dc 804	. . . . 5 |- (DECID ph -> (DECID ps -> ((-. ph /\ ps) <-> -. (ph \/ -. ps))))
2	1	imp 115	. . . 4 |- ((DECID ph /\ DECID ps) -> ((-. ph /\ ps) <-> -. (ph \/ -. ps)))
3		dcn 745	. . . . . . . . 9 |- (DECID ps -> DECID -. ps)
4	3	anim2i 324	. . . . . . . 8 |- ((DECID ph /\ DECID ps) -> (DECID ph /\ DECID -. ps))
5		dcor 842	. . . . . . . . 9 |- (DECID ph -> (DECID -. ps -> DECID (ph \/ -. ps)))
6	5	imp 115	. . . . . . . 8 |- ((DECID ph /\ DECID -. ps) -> DECID (ph \/ -. ps))
7	4, 6	syl 14	. . . . . . 7 |- ((DECID ph /\ DECID ps) -> DECID (ph \/ -. ps))
8		dcn 745	. . . . . . . . 9 |- (DECID ph -> DECID -. ph)
9		dcan 841	. . . . . . . . 9 |- (DECID -. ph -> (DECID ps -> DECID (-. ph /\ ps)))
10	8, 9	syl 14	. . . . . . . 8 |- (DECID ph -> (DECID ps -> DECID (-. ph /\ ps)))
11	10	imp 115	. . . . . . 7 |- ((DECID ph /\ DECID ps) -> DECID (-. ph /\ ps))
12	7, 11	jca 290	. . . . . 6 |- ((DECID ph /\ DECID ps) -> (DECID (ph \/ -. ps) /\ DECID (-. ph /\ ps)))
13		con2bidc 768	. . . . . . 7 |- (DECID (ph \/ -. ps) -> (DECID (-. ph /\ ps) -> (((ph \/ -. ps) <-> -. (-. ph /\ ps)) <-> ((-. ph /\ ps) <-> -. (ph \/ -. ps)))))
14	13	imp 115	. . . . . 6 |- ((DECID (ph \/ -. ps) /\ DECID (-. ph /\ ps)) -> (((ph \/ -. ps) <-> -. (-. ph /\ ps)) <-> ((-. ph /\ ps) <-> -. (ph \/ -. ps))))
15	12, 14	syl 14	. . . . 5 |- ((DECID ph /\ DECID ps) -> (((ph \/ -. ps) <-> -. (-. ph /\ ps)) <-> ((-. ph /\ ps) <-> -. (ph \/ -. ps))))
16	15	biimprd 147	. . . 4 |- ((DECID ph /\ DECID ps) -> (((-. ph /\ ps) <-> -. (ph \/ -. ps)) -> ((ph \/ -. ps) <-> -. (-. ph /\ ps))))
17	2, 16	mpd 13	. . 3 |- ((DECID ph /\ DECID ps) -> ((ph \/ -. ps) <-> -. (-. ph /\ ps)))
18	17	bicomd 129	. 2 |- ((DECID ph /\ DECID ps) -> (-. (-. ph /\ ps) <-> (ph \/ -. ps)))
19	18	ex 108	1 |- (DECID ph -> (DECID ps -> (-. (-. ph /\ ps) <-> (ph \/ -. ps))))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628  DECID wdc 741

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629

This theorem depends on definitions:  df-bi 110  df-dc 742

This theorem is referenced by: (None)