meran1 - Mathbox for Anthony Hart

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

Theorem meran1 30107

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 383	. . . . . 6 $\/$
2		olc 382	. . . . . 6 $\/$
3	1, 2	ja 161	. . . . 5 $\/$
4	3	imim1i 58	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
5		pm2.24 109	. . . . . 6
6		idd 24	. . . . . 6
7	5, 6	jaod 378	. . . . 5 $\/$
8	7	com12 31	. . . 4 $\/$
9		pm1.5 520	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
10		pm2.3 570	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
11		pm1.5 520	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
12		pm2.21 108	. . . . . . . . . . . . 13
13		mth8 146	. . . . . . . . . . . . 13
14	12, 13	imim12i 57	. . . . . . . . . . . 12
15	14	pm2.43d 48	. . . . . . . . . . 11
16	15	con4d 105	. . . . . . . . . 10
17		imor 410	. . . . . . . . . 10 $\/$
18		imor 410	. . . . . . . . . 10 $\/$
19	16, 17, 18	3imtr3i 265	. . . . . . . . 9 $\/$ $\/$
20	19	orim2i 516	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
21		pm1.5 520	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
22	10, 11, 20, 21	4syl 21	. . . . . . 7 $\/$ $\/$ $\/$ $\/$
23	22	orim2i 516	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
24		pm1.5 520	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
25	9, 23, 24	3syl 20	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
26		imor 410	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
27		imor 410	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
28	25, 26, 27	3imtr4i 266	. . . 4 $\/$ $\/$ $\/$ $\/$
29	4, 8, 28	syl2im 38	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
30		imor 410	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
31		imor 410	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
32	29, 30, 31	3imtr3i 265	. 2 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
33	32	imori 411	1 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 366

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 185 df-or 368

This theorem is referenced by: meran2 30108 meran3 30109