Theorem arg-ax 30887

Description: ? (Contributed by Anthony Hart, 14-Aug-2011.)

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		df-nan 1380	. . . . 5 |- ( ( th -/\ ch ) <-> -. ( th /\ ch ) )
2		pm4.57 499	. . . . . . . 8 |- ( -. ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) <-> ( ( ch /\ th ) \/ ( ph /\ th ) ) )
3		orel2 384	. . . . . . . . . . . . 13 |- ( -. ph -> ( ( ch \/ ph ) -> ch ) )
4	3	com12 32	. . . . . . . . . . . 12 |- ( ( ch \/ ph ) -> ( -. ph -> ch ) )
5		simpr 462	. . . . . . . . . . . . 13 |- ( ( ps /\ ch ) -> ch )
6	5	a1i 11	. . . . . . . . . . . 12 |- ( ( ch \/ ph ) -> ( ( ps /\ ch ) -> ch ) )
7	4, 6	jad 165	. . . . . . . . . . 11 |- ( ( ch \/ ph ) -> ( ( ph -> ( ps /\ ch ) ) -> ch ) )
8	7	com12 32	. . . . . . . . . 10 |- ( ( ph -> ( ps /\ ch ) ) -> ( ( ch \/ ph ) -> ch ) )
9		pm3.45 842	. . . . . . . . . . . 12 |- ( ( ch -> ch ) -> ( ( ch /\ th ) -> ( ch /\ th ) ) )
10		pm3.45 842	. . . . . . . . . . . 12 |- ( ( ph -> ch ) -> ( ( ph /\ th ) -> ( ch /\ th ) ) )
11	9, 10	anim12i 568	. . . . . . . . . . 11 |- ( ( ( ch -> ch ) /\ ( ph -> ch ) ) -> ( ( ( ch /\ th ) -> ( ch /\ th ) ) /\ ( ( ph /\ th ) -> ( ch /\ th ) ) ) )
12		jaob 790	. . . . . . . . . . 11 |- ( ( ( ch \/ ph ) -> ch ) <-> ( ( ch -> ch ) /\ ( ph -> ch ) ) )
13		jaob 790	. . . . . . . . . . 11 |- ( ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( ch /\ th ) ) <-> ( ( ( ch /\ th ) -> ( ch /\ th ) ) /\ ( ( ph /\ th ) -> ( ch /\ th ) ) ) )
14	11, 12, 13	3imtr4i 269	. . . . . . . . . 10 |- ( ( ( ch \/ ph ) -> ch ) -> ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( ch /\ th ) ) )
15	8, 14	syl 17	. . . . . . . . 9 |- ( ( ph -> ( ps /\ ch ) ) -> ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( ch /\ th ) ) )
16		pm3.22 450	. . . . . . . . 9 |- ( ( ch /\ th ) -> ( th /\ ch ) )
17	15, 16	syl6 34	. . . . . . . 8 |- ( ( ph -> ( ps /\ ch ) ) -> ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( th /\ ch ) ) )
18	2, 17	syl5bi 220	. . . . . . 7 |- ( ( ph -> ( ps /\ ch ) ) -> ( -. ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) -> ( th /\ ch ) ) )
19	18	con1d 127	. . . . . 6 |- ( ( ph -> ( ps /\ ch ) ) -> ( -. ( th /\ ch ) -> ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) ) )
20		df-nan 1380	. . . . . . . 8 |- ( ( ch -/\ th ) <-> -. ( ch /\ th ) )
21	20	biimpri 209	. . . . . . 7 |- ( -. ( ch /\ th ) -> ( ch -/\ th ) )
22		df-nan 1380	. . . . . . . 8 |- ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
23	22	biimpri 209	. . . . . . 7 |- ( -. ( ph /\ th ) -> ( ph -/\ th ) )
24	21, 23	anim12i 568	. . . . . 6 |- ( ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) )
25	19, 24	syl6 34	. . . . 5 |- ( ( ph -> ( ps /\ ch ) ) -> ( -. ( th /\ ch ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) ) )
26	1, 25	syl5bi 220	. . . 4 |- ( ( ph -> ( ps /\ ch ) ) -> ( ( th -/\ ch ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) ) )
27		nannan 1384	. . . 4 |- ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
28		nannan 1384	. . . 4 |- ( ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) <-> ( ( th -/\ ch ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) ) )
29	26, 27, 28	3imtr4i 269	. . 3 |- ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) )
30	29	ancli 553	. 2 |- ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( ph -/\ ( ps -/\ ch ) ) /\ ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
31		nannan 1384	. 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 212	1 |- ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 369   /\ wa 370   -/\ wnan 1379

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

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-nan 1380

This theorem is referenced by: (None)