meran1 - Mathbox for Anthony Hart

	Mathbox for Anthony Hart		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > meran1		Structured version Visualization version Unicode version

Theorem meran1 32410

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

**Assertion**
Ref	Expression
meran1	$\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

**Proof of Theorem meran1**
Step	Hyp	Ref	Expression
1		orc 400	. . . . . 6 $\/$
2		olc 399	. . . . . 6 $\/$
3	1, 2	ja 173	. . . . 5 $\/$
4	3	imim1i 63	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
5		pm2.24 121	. . . . . 6
6		idd 24	. . . . . 6
7	5, 6	jaod 395	. . . . 5 $\/$
8	7	com12 32	. . . 4 $\/$
9		pm1.5 544	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
10		pm2.3 596	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
11		pm1.5 544	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
12		pm2.21 120	. . . . . . . . . . . . 13
13		mth8 158	. . . . . . . . . . . . 13
14	12, 13	imim12i 62	. . . . . . . . . . . 12
15	14	pm2.43d 53	. . . . . . . . . . 11
16	15	con4d 114	. . . . . . . . . 10
17		imor 428	. . . . . . . . . 10 $\/$
18		imor 428	. . . . . . . . . 10 $\/$
19	16, 17, 18	3imtr3i 280	. . . . . . . . 9 $\/$ $\/$
20	19	orim2i 540	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
21		pm1.5 544	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
22	10, 11, 20, 21	4syl 19	. . . . . . 7 $\/$ $\/$ $\/$ $\/$
23	22	orim2i 540	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
24		pm1.5 544	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
25	9, 23, 24	3syl 18	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
26		imor 428	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
27		imor 428	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
28	25, 26, 27	3imtr4i 281	. . . 4 $\/$ $\/$ $\/$ $\/$
29	4, 8, 28	syl2im 40	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
30		imor 428	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
31		imor 428	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
32	29, 30, 31	3imtr3i 280	. 2 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
33	32	imori 429	1 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 383

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-or 385

This theorem is referenced by: meran2 32411 meran3 32412