Metamath Proof Explorer

Theorem lukshef-ax2

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

Ref Expression
Assertion lukshef-ax2 
|- ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ch -/\ ph ) ) -/\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nannan 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
2 1 biimpi 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -> ( ph -> ( ps /\ ch ) ) )
3 simpr 
 |-  ( ( ps /\ ch ) -> ch )
4 3 imim2i 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ch ) )
5 simpl 
 |-  ( ( ps /\ ch ) -> ps )
6 5 imim2i 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ps ) )
7 pm2.27 
 |-  ( ph -> ( ( ph -> ps ) -> ps ) )
8 7 anim2d 
 |-  ( ph -> ( ( th /\ ( ph -> ps ) ) -> ( th /\ ps ) ) )
9 8 expdimp 
 |-  ( ( ph /\ th ) -> ( ( ph -> ps ) -> ( th /\ ps ) ) )
10 6 9 syl5com 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( ph /\ th ) -> ( th /\ ps ) ) )
11 ancr 
 |-  ( ( ph -> ch ) -> ( ph -> ( ch /\ ph ) ) )
12 11 anim1i 
 |-  ( ( ( ph -> ch ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) -> ( ( ph -> ( ch /\ ph ) ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) )
13 4 10 12 syl2anc 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( ph -> ( ch /\ ph ) ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) )
14 con3 
 |-  ( ( ( ph /\ th ) -> ( th /\ ps ) ) -> ( -. ( th /\ ps ) -> -. ( ph /\ th ) ) )
15 df-nan 
 |-  ( ( th -/\ ps ) <-> -. ( th /\ ps ) )
16 df-nan 
 |-  ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
17 14 15 16 3imtr4g 
 |-  ( ( ( ph /\ th ) -> ( th /\ ps ) ) -> ( ( th -/\ ps ) -> ( ph -/\ th ) ) )
18 17 anim2i 
 |-  ( ( ( ph -> ( ch /\ ph ) ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) -> ( ( ph -> ( ch /\ ph ) ) /\ ( ( th -/\ ps ) -> ( ph -/\ th ) ) ) )
19 nannan 
 |-  ( ( ph -/\ ( ch -/\ ph ) ) <-> ( ph -> ( ch /\ ph ) ) )
20 19 biimpri 
 |-  ( ( ph -> ( ch /\ ph ) ) -> ( ph -/\ ( ch -/\ ph ) ) )
21 nanim 
 |-  ( ( ( th -/\ ps ) -> ( ph -/\ th ) ) <-> ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
22 21 biimpi 
 |-  ( ( ( th -/\ ps ) -> ( ph -/\ th ) ) -> ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
23 20 22 anim12i 
 |-  ( ( ( ph -> ( ch /\ ph ) ) /\ ( ( th -/\ ps ) -> ( ph -/\ th ) ) ) -> ( ( ph -/\ ( ch -/\ ph ) ) /\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
24 2 13 18 23 4syl 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( ph -/\ ( ch -/\ ph ) ) /\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
25 nannan 
 |-  ( ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ch -/\ ph ) ) -/\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) <-> ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( ph -/\ ( ch -/\ ph ) ) /\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) )
26 24 25 mpbir 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ch -/\ ph ) ) -/\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )