sbequilem - Intuitionistic Logic Explorer

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

Theorem sbequilem 1719

Description: Propositional logic lemma used in the sbequi 1720 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 257	. . . . . . . . 9 $\/$ $/\$ $\/$
4		andi 731	. . . . . . . . 9 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
5	3, 4	mpbi 133	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $/\$
6		andir 732	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
7		andir 732	. . . . . . . . 9 $\/$ $/\$ $/\$ $\/$ $/\$
8	6, 7	orbi12i 681	. . . . . . . 8 $\/$ $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	5, 8	mpbi 133	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
10		pm3.43 534	. . . . . . . . . 10 $/\$ $/\$
11		pm3.33 327	. . . . . . . . . 10 $/\$
12	10, 11	syl6 29	. . . . . . . . 9 $/\$
13	12	orim2i 678	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$
14	13	orim2i 678	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
15	9, 14	ax-mp 7	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
16		simpr 103	. . . . . . . 8 $\/$ $/\$
17	6, 16	sylbir 125	. . . . . . 7 $/\$ $\/$ $/\$
18	17	orim1i 677	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
19	15, 18	ax-mp 7	. . . . 5 $\/$ $/\$ $\/$
20		simpl 102	. . . . . . 7 $/\$
21	20	orim1i 677	. . . . . 6 $/\$ $\/$ $\/$
22	21	orim2i 678	. . . . 5 $\/$ $/\$ $\/$ $\/$ $\/$
23	19, 22	ax-mp 7	. . . 4 $\/$ $\/$
24		orass 684	. . . 4 $\/$ $\/$ $\/$ $\/$
25	23, 24	mpbir 134	. . 3 $\/$ $\/$
26		orcom 647	. . . 4 $\/$ $\/$
27	26	orbi1i 680	. . 3 $\/$ $\/$ $\/$ $\/$
28	25, 27	mpbi 133	. 2 $\/$ $\/$
29		orass 684	. 2 $\/$ $\/$ $\/$ $\/$
30	28, 29	mpbi 133	1 $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 97 $\/$ wo 629

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630

This theorem depends on definitions: df-bi 110

This theorem is referenced by: sbequi 1720