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 31142

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 392	. . . . . 6 $\/$
2		olc 391	. . . . . 6 $\/$
3	1, 2	ja 166	. . . . 5 $\/$
4	3	imim1i 59	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
5		pm2.24 112	. . . . . 6
6		idd 24	. . . . . 6
7	5, 6	jaod 387	. . . . 5 $\/$
8	7	com12 31	. . . 4 $\/$
9		pm1.5 531	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
10		pm2.3 582	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
11		pm1.5 531	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
12		pm2.21 111	. . . . . . . . . . . . 13
13		mth8 151	. . . . . . . . . . . . 13
14	12, 13	imim12i 58	. . . . . . . . . . . 12
15	14	pm2.43d 49	. . . . . . . . . . 11
16	15	con4d 108	. . . . . . . . . 10
17		imor 419	. . . . . . . . . 10 $\/$
18		imor 419	. . . . . . . . . 10 $\/$
19	16, 17, 18	3imtr3i 273	. . . . . . . . 9 $\/$ $\/$
20	19	orim2i 527	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
21		pm1.5 531	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
22	10, 11, 20, 21	4syl 19	. . . . . . 7 $\/$ $\/$ $\/$ $\/$
23	22	orim2i 527	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
24		pm1.5 531	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
25	9, 23, 24	3syl 18	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
26		imor 419	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
27		imor 419	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
28	25, 26, 27	3imtr4i 274	. . . 4 $\/$ $\/$ $\/$ $\/$
29	4, 8, 28	syl2im 38	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
30		imor 419	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
31		imor 419	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
32	29, 30, 31	3imtr3i 273	. 2 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
33	32	imori 420	1 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 375

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 190 df-or 377

This theorem is referenced by: meran2 31143 meran3 31144