sbequilem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > sbequilem		Unicode version

Theorem sbequilem 1852

Description: Propositional logic lemma used in the sbequi 1853 proof. (Contributed by Jim Kingdon, 1-Feb-2018.)

**Hypotheses**
Ref	Expression
sbequilem.1	$\/$
sbequilem.2	$\/$

**Assertion**
Ref	Expression
sbequilem	$\/$ $\/$

**Proof of Theorem sbequilem**
Step	Hyp	Ref	Expression
1		sbequilem.1	. . . . . . . . . 10 $\/$
2		sbequilem.2	. . . . . . . . . 10 $\/$
3	1, 2	pm3.2i 272	. . . . . . . . 9 $\/$ $/\$ $\/$
4		andi 819	. . . . . . . . 9 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
5	3, 4	mpbi 145	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $/\$
6		andir 820	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
7		andir 820	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
8	6, 7	orbi12i 765	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	5, 8	mpbi 145	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10		pm3.43 602	. . . . . . . . . 10 $/\$ $/\$
11		pm3.33 345	. . . . . . . . . 10 $/\$
12	10, 11	syl6 33	. . . . . . . . 9 $/\$
13	12	orim2i 762	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$
14	13	orim2i 762	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
15	9, 14	ax-mp 5	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
16		simpr 110	. . . . . . . 8 $\/$ $/\$
17	6, 16	sylbir 135	. . . . . . 7 $/\$ $\/$ $/\$
18	17	orim1i 761	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
19	15, 18	ax-mp 5	. . . . 5 $\/$ $/\$ $\/$
20		simpl 109	. . . . . . 7 $/\$
21	20	orim1i 761	. . . . . 6 $/\$ $\/$ $\/$
22	21	orim2i 762	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$
23	19, 22	ax-mp 5	. . . 4 $\/$ $\/$
24		orass 768	. . . 4 $\/$ $\/$ $\/$ $\/$
25	23, 24	mpbir 146	. . 3 $\/$ $\/$
26		orcom 729	. . . 4 $\/$ $\/$
27	26	orbi1i 764	. . 3 $\/$ $\/$ $\/$ $\/$
28	25, 27	mpbi 145	. 2 $\/$ $\/$
29		orass 768	. 2 $\/$ $\/$ $\/$ $\/$
30	28, 29	mpbi 145	1 $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104 $\/$ wo 709

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710

This theorem depends on definitions: df-bi 117

This theorem is referenced by: sbequi 1853