Metamath Proof Explorer

Theorem waj-ax

Description: A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson,Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 nannan 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
2 simpr 
 |-  ( ( ps /\ ch ) -> ch )
3 2 imim2i 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ch ) )
4 pm2.27 
 |-  ( ph -> ( ( ph -> ch ) -> ch ) )
5 4 anim2d 
 |-  ( ph -> ( ( th /\ ( ph -> ch ) ) -> ( th /\ ch ) ) )
6 5 expdimp 
 |-  ( ( ph /\ th ) -> ( ( ph -> ch ) -> ( th /\ ch ) ) )
7 3 6 syl5com 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( ph /\ th ) -> ( th /\ ch ) ) )
8 7 con3d 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( -. ( th /\ ch ) -> -. ( ph /\ th ) ) )
9 df-nan 
 |-  ( ( th -/\ ch ) <-> -. ( th /\ ch ) )
10 df-nan 
 |-  ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
11 8 9 10 3imtr4g 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( th -/\ ch ) -> ( ph -/\ th ) ) )
12 nanim 
 |-  ( ( ( th -/\ ch ) -> ( ph -/\ th ) ) <-> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
13 11 12 sylib 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
14 pm3.21 
 |-  ( ps -> ( ph -> ( ph /\ ps ) ) )
15 14 adantr 
 |-  ( ( ps /\ ch ) -> ( ph -> ( ph /\ ps ) ) )
16 15 com12 
 |-  ( ph -> ( ( ps /\ ch ) -> ( ph /\ ps ) ) )
17 16 a2i 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ( ph /\ ps ) ) )
18 nannan 
 |-  ( ( ph -/\ ( ph -/\ ps ) ) <-> ( ph -> ( ph /\ ps ) ) )
19 17 18 sylibr 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ph -/\ ( ph -/\ ps ) ) )
20 13 19 jca 
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) /\ ( ph -/\ ( ph -/\ ps ) ) ) )
21 1 20 sylbi 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) /\ ( ph -/\ ( ph -/\ ps ) ) ) )
22 nannan 
 |-  ( ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) -/\ ( ph -/\ ( ph -/\ ps ) ) ) ) <-> ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) /\ ( ph -/\ ( ph -/\ ps ) ) ) ) )
23 21 22 mpbir 
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) -/\ ( ph -/\ ( ph -/\ ps ) ) ) )