Theorem lukshef-ax2 14239

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

Assertion

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

Proof of Theorem lukshef-ax2

Step	Hyp	Ref	Expression
1		nic-justlem 1231	. . . 4 |- ((ph -/\ (ps -/\ ch)) <-> (ph -> (ps /\ ch)))
2	1	biimpi 168	. . 3 |- ((ph -/\ (ps -/\ ch)) -> (ph -> (ps /\ ch)))
3		simpr 350	. . . . . 6 |- ((ps /\ ch) -> ch)
4	3	imim2i 11	. . . . 5 |- ((ph -> (ps /\ ch)) -> (ph -> ch))
5		pm2.27 76	. . . . . . . 8 |- (ph -> ((ph -> ps) -> ps))
6	5	anim2d 620	. . . . . . 7 |- (ph -> ((th /\ (ph -> ps)) -> (th /\ ps)))
7	6	expdimp 406	. . . . . 6 |- ((ph /\ th) -> ((ph -> ps) -> (th /\ ps)))
8		simpl 346	. . . . . . 7 |- ((ps /\ ch) -> ps)
9	8	imim2i 11	. . . . . 6 |- ((ph -> (ps /\ ch)) -> (ph -> ps))
10	7, 9	syl5com 63	. . . . 5 |- ((ph -> (ps /\ ch)) -> ((ph /\ th) -> (th /\ ps)))
11		ancr 319	. . . . . 6 |- ((ph -> ch) -> (ph -> (ch /\ ph)))
12	11	anim1i 361	. . . . 5 |- (((ph -> ch) /\ ((ph /\ th) -> (th /\ ps))) -> ((ph -> (ch /\ ph)) /\ ((ph /\ th) -> (th /\ ps))))
13	4, 10, 12	syl11anc 524	. . . 4 |- ((ph -> (ps /\ ch)) -> ((ph -> (ch /\ ph)) /\ ((ph /\ th) -> (th /\ ps))))
14		con3 110	. . . . . 6 |- (((ph /\ th) -> (th /\ ps)) -> (-. (th /\ ps) -> -. (ph /\ th)))
15		df-nand 1230	. . . . . 6 |- ((th -/\ ps) <-> -. (th /\ ps))
16		df-nand 1230	. . . . . 6 |- ((ph -/\ th) <-> -. (ph /\ th))
17	14, 15, 16	3imtr4g 612	. . . . 5 |- (((ph /\ th) -> (th /\ ps)) -> ((th -/\ ps) -> (ph -/\ th)))
18	17	anim2i 362	. . . 4 |- (((ph -> (ch /\ ph)) /\ ((ph /\ th) -> (th /\ ps))) -> ((ph -> (ch /\ ph)) /\ ((th -/\ ps) -> (ph -/\ th))))
19	13, 18	syl 12	. . 3 |- ((ph -> (ps /\ ch)) -> ((ph -> (ch /\ ph)) /\ ((th -/\ ps) -> (ph -/\ th))))
20		nic-justlem 1231	. . . . 5 |- ((ph -/\ (ch -/\ ph)) <-> (ph -> (ch /\ ph)))
21	20	biimpri 169	. . . 4 |- ((ph -> (ch /\ ph)) -> (ph -/\ (ch -/\ ph)))
22		nic-justim 1232	. . . . 5 |- (((th -/\ ps) -> (ph -/\ th)) <-> ((th -/\ ps) -/\ ((ph -/\ th) -/\ (ph -/\ th))))
23	22	biimpi 168	. . . 4 |- (((th -/\ ps) -> (ph -/\ th)) -> ((th -/\ ps) -/\ ((ph -/\ th) -/\ (ph -/\ th))))
24	21, 23	anim12i 360	. . 3 |- (((ph -> (ch /\ ph)) /\ ((th -/\ ps) -> (ph -/\ th))) -> ((ph -/\ (ch -/\ ph)) /\ ((th -/\ ps) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
25	2, 19, 24	3syl 24	. 2 |- ((ph -/\ (ps -/\ ch)) -> ((ph -/\ (ch -/\ ph)) /\ ((th -/\ ps) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))
26		nic-justlem 1231	. 2 |- (((ph -/\ (ps -/\ ch)) -/\ ((ph -/\ (ch -/\ ph)) -/\ ((th -/\ ps) -/\ ((ph -/\ th) -/\ (ph -/\ th))))) <-> ((ph -/\ (ps -/\ ch)) -> ((ph -/\ (ch -/\ ph)) /\ ((th -/\ ps) -/\ ((ph -/\ th) -/\ (ph -/\ th))))))
27	25, 26	mpbir 207	1 |- ((ph -/\ (ps -/\ ch)) -/\ ((ph -/\ (ch -/\ ph)) -/\ ((th -/\ ps) -/\ ((ph -/\ th) -/\ (ph -/\ th)))))

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