Theorem waj-ax 14238

Description: A single axiom for propositional calculus offered by Wajsberg.

Assertion

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

Proof of Theorem waj-ax

Step	Hyp	Ref	Expression
1		nic-justlem 1231	. . 3 |- ((ph -/\ (ps -/\ ch)) <-> (ph -> (ps /\ ch)))
2		pm2.27 76	. . . . . . . . . 10 |- (ph -> ((ph -> ch) -> ch))
3	2	anim2d 620	. . . . . . . . 9 |- (ph -> ((th /\ (ph -> ch)) -> (th /\ ch)))
4	3	expdimp 406	. . . . . . . 8 |- ((ph /\ th) -> ((ph -> ch) -> (th /\ ch)))
5		simpr 350	. . . . . . . . 9 |- ((ps /\ ch) -> ch)
6	5	imim2i 11	. . . . . . . 8 |- ((ph -> (ps /\ ch)) -> (ph -> ch))
7	4, 6	syl5com 63	. . . . . . 7 |- ((ph -> (ps /\ ch)) -> ((ph /\ th) -> (th /\ ch)))
8	7	con3d 111	. . . . . 6 |- ((ph -> (ps /\ ch)) -> (-. (th /\ ch) -> -. (ph /\ th)))
9		df-nand 1230	. . . . . 6 |- ((th -/\ ch) <-> -. (th /\ ch))
10		df-nand 1230	. . . . . 6 |- ((ph -/\ th) <-> -. (ph /\ th))
11	8, 9, 10	3imtr4g 612	. . . . 5 |- ((ph -> (ps /\ ch)) -> ((th -/\ ch) -> (ph -/\ th)))
12		nic-justim 1232	. . . . 5 |- (((th -/\ ch) -> (ph -/\ th)) <-> ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))
13	11, 12	sylib 215	. . . 4 |- ((ph -> (ps /\ ch)) -> ((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))))
14		pm3.21 306	. . . . . . . 8 |- (ps -> (ph -> (ph /\ ps)))
15	14	adantr 425	. . . . . . 7 |- ((ps /\ ch) -> (ph -> (ph /\ ps)))
16	15	com12 14	. . . . . 6 |- (ph -> ((ps /\ ch) -> (ph /\ ps)))
17	16	a2i 10	. . . . 5 |- ((ph -> (ps /\ ch)) -> (ph -> (ph /\ ps)))
18		nic-justlem 1231	. . . . 5 |- ((ph -/\ (ph -/\ ps)) <-> (ph -> (ph /\ ps)))
19	17, 18	sylibr 217	. . . 4 |- ((ph -> (ps /\ ch)) -> (ph -/\ (ph -/\ ps)))
20	13, 19	jca 310	. . 3 |- ((ph -> (ps /\ ch)) -> (((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))) /\ (ph -/\ (ph -/\ ps))))
21	1, 20	sylbi 216	. 2 |- ((ph -/\ (ps -/\ ch)) -> (((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))) /\ (ph -/\ (ph -/\ ps))))
22		nic-justlem 1231	. 2 |- (((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 207	1 |- ((ph -/\ (ps -/\ ch)) -/\ (((th -/\ ch) -/\ ((ph -/\ th) -/\ (ph -/\ th))) -/\ (ph -/\ (ph -/\ ps))))

Syntax hints:  -. wn 2   -> wi 3   /\ 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-an 242  df-nand 1230

Copyright terms: Public domain