Theorem arg-ax 14240

Description: ?

Assertion

Ref	Expression
arg-ax	|- ((ph -/\ (ps -/\ ch)) -/\ ((ph -/\ (ps -/\ ch)) -/\ ((th -/\ ch) -/\ ((ch -/\ th) -/\ (ph -/\ th)))))

Proof of Theorem arg-ax

Step	Hyp	Ref	Expression
1		orel2 272	. . . . . . . . . . . 12 |- (-. ph -> ((ch \/ ph) -> ch))
2	1	com12 14	. . . . . . . . . . 11 |- ((ch \/ ph) -> (-. ph -> ch))
3		simpr 350	. . . . . . . . . . . 12 |- ((ps /\ ch) -> ch)
4	3	a1i 8	. . . . . . . . . . 11 |- ((ch \/ ph) -> ((ps /\ ch) -> ch))
5	2, 4	jad 156	. . . . . . . . . 10 |- ((ch \/ ph) -> ((ph -> (ps /\ ch)) -> ch))
6	5	com12 14	. . . . . . . . 9 |- ((ph -> (ps /\ ch)) -> ((ch \/ ph) -> ch))
7		pm3.45 621	. . . . . . . . . . 11 |- ((ch -> ch) -> ((ch /\ th) -> (ch /\ th)))
8		pm3.45 621	. . . . . . . . . . 11 |- ((ph -> ch) -> ((ph /\ th) -> (ch /\ th)))
9	7, 8	anim12i 360	. . . . . . . . . 10 |- (((ch -> ch) /\ (ph -> ch)) -> (((ch /\ th) -> (ch /\ th)) /\ ((ph /\ th) -> (ch /\ th))))
10		jaob 467	. . . . . . . . . 10 |- (((ch \/ ph) -> ch) <-> ((ch -> ch) /\ (ph -> ch)))
11		jaob 467	. . . . . . . . . 10 |- ((((ch /\ th) \/ (ph /\ th)) -> (ch /\ th)) <-> (((ch /\ th) -> (ch /\ th)) /\ ((ph /\ th) -> (ch /\ th))))
12	9, 10, 11	3imtr4i 236	. . . . . . . . 9 |- (((ch \/ ph) -> ch) -> (((ch /\ th) \/ (ph /\ th)) -> (ch /\ th)))
13		pm3.22 486	. . . . . . . . . 10 |- ((ch /\ th) -> (th /\ ch))
14	13	imim2i 11	. . . . . . . . 9 |- ((((ch /\ th) \/ (ph /\ th)) -> (ch /\ th)) -> (((ch /\ th) \/ (ph /\ th)) -> (th /\ ch)))
15	6, 12, 14	3syl 24	. . . . . . . 8 |- ((ph -> (ps /\ ch)) -> (((ch /\ th) \/ (ph /\ th)) -> (th /\ ch)))
16		pm4.57 340	. . . . . . . 8 |- (-. (-. (ch /\ th) /\ -. (ph /\ th)) <-> ((ch /\ th) \/ (ph /\ th)))
17	15, 16	syl5ib 223	. . . . . . 7 |- ((ph -> (ps /\ ch)) -> (-. (-. (ch /\ th) /\ -. (ph /\ th)) -> (th /\ ch)))
18	17	con1d 109	. . . . . 6 |- ((ph -> (ps /\ ch)) -> (-. (th /\ ch) -> (-. (ch /\ th) /\ -. (ph /\ th))))
19		df-nand 1230	. . . . . . . 8 |- ((ch -/\ th) <-> -. (ch /\ th))
20	19	biimpri 169	. . . . . . 7 |- (-. (ch /\ th) -> (ch -/\ th))
21		df-nand 1230	. . . . . . . 8 |- ((ph -/\ th) <-> -. (ph /\ th))
22	21	biimpri 169	. . . . . . 7 |- (-. (ph /\ th) -> (ph -/\ th))
23	20, 22	anim12i 360	. . . . . 6 |- ((-. (ch /\ th) /\ -. (ph /\ th)) -> ((ch -/\ th) /\ (ph -/\ th)))
24	18, 23	syl6 25	. . . . 5 |- ((ph -> (ps /\ ch)) -> (-. (th /\ ch) -> ((ch -/\ th) /\ (ph -/\ th))))
25		df-nand 1230	. . . . 5 |- ((th -/\ ch) <-> -. (th /\ ch))
26	24, 25	syl5ib 223	. . . 4 |- ((ph -> (ps /\ ch)) -> ((th -/\ ch) -> ((ch -/\ th) /\ (ph -/\ th))))
27		nic-justlem 1231	. . . 4 |- ((ph -/\ (ps -/\ ch)) <-> (ph -> (ps /\ ch)))
28		nic-justlem 1231	. . . 4 |- (((th -/\ ch) -/\ ((ch -/\ th) -/\ (ph -/\ th))) <-> ((th -/\ ch) -> ((ch -/\ th) /\ (ph -/\ th))))
29	26, 27, 28	3imtr4i 236	. . 3 |- ((ph -/\ (ps -/\ ch)) -> ((th -/\ ch) -/\ ((ch -/\ th) -/\ (ph -/\ th))))
30	29	ancli 320	. 2 |- ((ph -/\ (ps -/\ ch)) -> ((ph -/\ (ps -/\ ch)) /\ ((th -/\ ch) -/\ ((ch -/\ th) -/\ (ph -/\ th)))))
31		nic-justlem 1231	. 2 |- (((ph -/\ (ps -/\ ch)) -/\ ((ph -/\ (ps -/\ ch)) -/\ ((th -/\ ch) -/\ ((ch -/\ th) -/\ (ph -/\ th))))) <-> ((ph -/\ (ps -/\ ch)) -> ((ph -/\ (ps -/\ ch)) /\ ((th -/\ ch) -/\ ((ch -/\ th) -/\ (ph -/\ th))))))
32	30, 31	mpbir 207	1 |- ((ph -/\ (ps -/\ ch)) -/\ ((ph -/\ (ps -/\ ch)) -/\ ((th -/\ ch) -/\ ((ch -/\ th) -/\ (ph -/\ th)))))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240   -/\ wnand 1229

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  df-nand 1230

Copyright terms: Public domain