19.33b - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem 19.33b 1444

Description: The antecedent provides a condition implying the converse of 19.33 1443. Compare Theorem 19.33 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.)

**Assertion**
Ref	Expression
19.33b	$/\$ $\/$ $\/$

**Proof of Theorem 19.33b**
Step	Hyp	Ref	Expression
1		ianor 329	. . 3 $/\$ $\/$
2		alnex 1380	. . . . 5
3		biorf 807	. . . . . . . 8 $\/$
4	3	alimi 1338	. . . . . . 7 $\/$
5		albi 1344	. . . . . . 7 $\/$ $\/$
6	4, 5	syl 12	. . . . . 6 $\/$
7		olc 290	. . . . . 6 $\/$
8	6, 7	syl6bir 232	. . . . 5 $\/$ $\/$
9	2, 8	sylbir 218	. . . 4 $\/$ $\/$
10		orc 291	. . . . . . 7 $\/$
11	10	a1i 8	. . . . . 6 $\/$
12		pm2.21 92	. . . . . 6 $\/$
13	11, 12	jaod 469	. . . . 5 $\/$ $\/$
14		19.30 1436	. . . . 5 $\/$ $\/$
15	13, 14	syl5 20	. . . 4 $\/$ $\/$
16	9, 15	jaoi 368	. . 3 $\/$ $\/$ $\/$
17	1, 16	sylbi 216	. 2 $/\$ $\/$ $\/$
18		19.33 1443	. 2 $\/$ $\/$
19	17, 18	impbid1 575	1 $/\$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $\/$ wo 239 $/\$ wa 240

wal 1296

wex 1326

This theorem is referenced by: kmlem16 5942

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1305 ax-4 1319 ax-5o 1321

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327