Metamath Proof Explorer

Theorem arg-ax

Description: A single axiom for propositional calculus discovered by Ken Harris and Branden Fitelson. See: Fitelson,Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom HF1 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 df-nan 
 |-  ( ( th -/\ ch ) <-> -. ( th /\ ch ) )
2 pm4.57 
 |-  ( -. ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) <-> ( ( ch /\ th ) \/ ( ph /\ th ) ) )
3 orel2 
 |-  ( -. ph -> ( ( ch \/ ph ) -> ch ) )
4 3 com12 
 |-  ( ( ch \/ ph ) -> ( -. ph -> ch ) )
5 simpr 
 |-  ( ( ps /\ ch ) -> ch )
6 5 a1i 
 |-  ( ( ch \/ ph ) -> ( ( ps /\ ch ) -> ch ) )
7 4 6 jad 
 |-  ( ( ch \/ ph ) -> ( ( ph -> ( ps /\ ch ) ) -> ch ) )
8 7 com12 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( ch \/ ph ) -> ch ) )
9 pm3.45 
 |-  ( ( ch -> ch ) -> ( ( ch /\ th ) -> ( ch /\ th ) ) )
10 pm3.45 
 |-  ( ( ph -> ch ) -> ( ( ph /\ th ) -> ( ch /\ th ) ) )
11 9 10 anim12i 
 |-  ( ( ( ch -> ch ) /\ ( ph -> ch ) ) -> ( ( ( ch /\ th ) -> ( ch /\ th ) ) /\ ( ( ph /\ th ) -> ( ch /\ th ) ) ) )
12 jaob 
 |-  ( ( ( ch \/ ph ) -> ch ) <-> ( ( ch -> ch ) /\ ( ph -> ch ) ) )
13 jaob 
 |-  ( ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( ch /\ th ) ) <-> ( ( ( ch /\ th ) -> ( ch /\ th ) ) /\ ( ( ph /\ th ) -> ( ch /\ th ) ) ) )
14 11 12 13 3imtr4i 
 |-  ( ( ( ch \/ ph ) -> ch ) -> ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( ch /\ th ) ) )
15 8 14 syl 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( ch /\ th ) ) )
16 pm3.22 
 |-  ( ( ch /\ th ) -> ( th /\ ch ) )
17 15 16 syl6 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( ( ch /\ th ) \/ ( ph /\ th ) ) -> ( th /\ ch ) ) )
18 2 17 syl5bi 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( -. ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) -> ( th /\ ch ) ) )
19 18 con1d 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( -. ( th /\ ch ) -> ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) ) )
20 df-nan 
 |-  ( ( ch -/\ th ) <-> -. ( ch /\ th ) )
21 20 biimpri 
 |-  ( -. ( ch /\ th ) -> ( ch -/\ th ) )
22 df-nan 
 |-  ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
23 22 biimpri 
 |-  ( -. ( ph /\ th ) -> ( ph -/\ th ) )
24 21 23 anim12i 
 |-  ( ( -. ( ch /\ th ) /\ -. ( ph /\ th ) ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) )
25 19 24 syl6 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( -. ( th /\ ch ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) ) )
26 1 25 syl5bi 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( th -/\ ch ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) ) )
27 nannan 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
28 nannan 
 |-  ( ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) <-> ( ( th -/\ ch ) -> ( ( ch -/\ th ) /\ ( ph -/\ th ) ) ) )
29 26 27 28 3imtr4i 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) )
30 29 ancli 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( ph -/\ ( ps -/\ ch ) ) /\ ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
31 nannan 
 |-  ( ( ( 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 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) ) )