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 31020

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 386	. . . . . 6 $\/$
2		olc 385	. . . . . 6 $\/$
3	1, 2	ja 164	. . . . 5 $\/$
4	3	imim1i 60	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
5		pm2.24 112	. . . . . 6
6		idd 25	. . . . . 6
7	5, 6	jaod 381	. . . . 5 $\/$
8	7	com12 32	. . . 4 $\/$
9		pm1.5 524	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
10		pm2.3 574	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
11		pm1.5 524	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
12		pm2.21 111	. . . . . . . . . . . . 13
13		mth8 149	. . . . . . . . . . . . 13
14	12, 13	imim12i 59	. . . . . . . . . . . 12
15	14	pm2.43d 50	. . . . . . . . . . 11
16	15	con4d 108	. . . . . . . . . 10
17		imor 413	. . . . . . . . . 10 $\/$
18		imor 413	. . . . . . . . . 10 $\/$
19	16, 17, 18	3imtr3i 268	. . . . . . . . 9 $\/$ $\/$
20	19	orim2i 520	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
21		pm1.5 524	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$
22	10, 11, 20, 21	4syl 19	. . . . . . 7 $\/$ $\/$ $\/$ $\/$
23	22	orim2i 520	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
24		pm1.5 524	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
25	9, 23, 24	3syl 18	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
26		imor 413	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
27		imor 413	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
28	25, 26, 27	3imtr4i 269	. . . 4 $\/$ $\/$ $\/$ $\/$
29	4, 8, 28	syl2im 39	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
30		imor 413	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
31		imor 413	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
32	29, 30, 31	3imtr3i 268	. 2 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
33	32	imori 414	1 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 369

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 188 df-or 371

This theorem is referenced by: meran2 31021 meran3 31022