sbequilem - Intuitionistic Logic Explorer

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

Theorem sbequilem 1826

Description: Propositional logic lemma used in the sbequi 1827 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 270	. . . . . . . . 9 $\/$ $/\$ $\/$
4		andi 808	. . . . . . . . 9 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
5	3, 4	mpbi 144	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $/\$
6		andir 809	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
7		andir 809	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
8	6, 7	orbi12i 754	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	5, 8	mpbi 144	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10		pm3.43 592	. . . . . . . . . 10 $/\$ $/\$
11		pm3.33 343	. . . . . . . . . 10 $/\$
12	10, 11	syl6 33	. . . . . . . . 9 $/\$
13	12	orim2i 751	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$
14	13	orim2i 751	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
15	9, 14	ax-mp 5	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
16		simpr 109	. . . . . . . 8 $\/$ $/\$
17	6, 16	sylbir 134	. . . . . . 7 $/\$ $\/$ $/\$
18	17	orim1i 750	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
19	15, 18	ax-mp 5	. . . . 5 $\/$ $/\$ $\/$
20		simpl 108	. . . . . . 7 $/\$
21	20	orim1i 750	. . . . . 6 $/\$ $\/$ $\/$
22	21	orim2i 751	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$
23	19, 22	ax-mp 5	. . . 4 $\/$ $\/$
24		orass 757	. . . 4 $\/$ $\/$ $\/$ $\/$
25	23, 24	mpbir 145	. . 3 $\/$ $\/$
26		orcom 718	. . . 4 $\/$ $\/$
27	26	orbi1i 753	. . 3 $\/$ $\/$ $\/$ $\/$
28	25, 27	mpbi 144	. 2 $\/$ $\/$
29		orass 757	. 2 $\/$ $\/$ $\/$ $\/$
30	28, 29	mpbi 144	1 $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103 $\/$ wo 698

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

This theorem depends on definitions: df-bi 116

This theorem is referenced by: sbequi 1827