Theorem lukshef-ax2 32414

Description: A single axiom for propositional calculus offered by Lukasiewicz. (Contributed by Anthony Hart, 14-Aug-2011.)

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		nannan 1451	. . . 4 |- ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
2	1	biimpi 206	. . 3 |- ( ( ph -/\ ( ps -/\ ch ) ) -> ( ph -> ( ps /\ ch ) ) )
3		simpr 477	. . . . 5 |- ( ( ps /\ ch ) -> ch )
4	3	imim2i 16	. . . 4 |- ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ch ) )
5		simpl 473	. . . . . 6 |- ( ( ps /\ ch ) -> ps )
6	5	imim2i 16	. . . . 5 |- ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ps ) )
7		pm2.27 42	. . . . . . 7 |- ( ph -> ( ( ph -> ps ) -> ps ) )
8	7	anim2d 589	. . . . . 6 |- ( ph -> ( ( th /\ ( ph -> ps ) ) -> ( th /\ ps ) ) )
9	8	expdimp 453	. . . . 5 |- ( ( ph /\ th ) -> ( ( ph -> ps ) -> ( th /\ ps ) ) )
10	6, 9	syl5com 31	. . . 4 |- ( ( ph -> ( ps /\ ch ) ) -> ( ( ph /\ th ) -> ( th /\ ps ) ) )
11		ancr 572	. . . . 5 |- ( ( ph -> ch ) -> ( ph -> ( ch /\ ph ) ) )
12	11	anim1i 592	. . . 4 |- ( ( ( ph -> ch ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) -> ( ( ph -> ( ch /\ ph ) ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) )
13	4, 10, 12	syl2anc 693	. . 3 |- ( ( ph -> ( ps /\ ch ) ) -> ( ( ph -> ( ch /\ ph ) ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) )
14		con3 149	. . . . 5 |- ( ( ( ph /\ th ) -> ( th /\ ps ) ) -> ( -. ( th /\ ps ) -> -. ( ph /\ th ) ) )
15		df-nan 1448	. . . . 5 |- ( ( th -/\ ps ) <-> -. ( th /\ ps ) )
16		df-nan 1448	. . . . 5 |- ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
17	14, 15, 16	3imtr4g 285	. . . 4 |- ( ( ( ph /\ th ) -> ( th /\ ps ) ) -> ( ( th -/\ ps ) -> ( ph -/\ th ) ) )
18	17	anim2i 593	. . 3 |- ( ( ( ph -> ( ch /\ ph ) ) /\ ( ( ph /\ th ) -> ( th /\ ps ) ) ) -> ( ( ph -> ( ch /\ ph ) ) /\ ( ( th -/\ ps ) -> ( ph -/\ th ) ) ) )
19		nannan 1451	. . . . 5 |- ( ( ph -/\ ( ch -/\ ph ) ) <-> ( ph -> ( ch /\ ph ) ) )
20	19	biimpri 218	. . . 4 |- ( ( ph -> ( ch /\ ph ) ) -> ( ph -/\ ( ch -/\ ph ) ) )
21		nanim 1452	. . . . 5 |- ( ( ( th -/\ ps ) -> ( ph -/\ th ) ) <-> ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
22	21	biimpi 206	. . . 4 |- ( ( ( th -/\ ps ) -> ( ph -/\ th ) ) -> ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
23	20, 22	anim12i 590	. . 3 |- ( ( ( ph -> ( ch /\ ph ) ) /\ ( ( th -/\ ps ) -> ( ph -/\ th ) ) ) -> ( ( ph -/\ ( ch -/\ ph ) ) /\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
24	2, 13, 18, 23	4syl 19	. 2 |- ( ( ph -/\ ( ps -/\ ch ) ) -> ( ( ph -/\ ( ch -/\ ph ) ) /\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
25		nannan 1451	. 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 ) ) ) ) ) )
26	24, 25	mpbir 221	1 |- ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ch -/\ ph ) ) -/\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   -/\ wnan 1447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-nan 1448

This theorem is referenced by: (None)