19.33b - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 19.33b		Structured version Visualization version Unicode version

Theorem 19.33b 1813

Description: The antecedent provides a condition implying the converse of 19.33 1812. (Contributed by NM, 27-Mar-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 5-Jul-2014.)

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

**Proof of Theorem 19.33b**
Step	Hyp	Ref	Expression
1		ianor 509	. . 3 $/\$ $\/$
2		alnex 1706	. . . . . 6
3		pm2.53 388	. . . . . . 7 $\/$
4	3	al2imi 1743	. . . . . 6 $\/$
5	2, 4	syl5bir 233	. . . . 5 $\/$
6		olc 399	. . . . 5 $\/$
7	5, 6	syl6com 37	. . . 4 $\/$ $\/$
8		19.30 1809	. . . . . . 7 $\/$ $\/$
9	8	orcomd 403	. . . . . 6 $\/$ $\/$
10	9	ord 392	. . . . 5 $\/$
11		orc 400	. . . . 5 $\/$
12	10, 11	syl6com 37	. . . 4 $\/$ $\/$
13	7, 12	jaoi 394	. . 3 $\/$ $\/$ $\/$
14	1, 13	sylbi 207	. 2 $/\$ $\/$ $\/$
15		19.33 1812	. 2 $\/$ $\/$
16	14, 15	impbid1 215	1 $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wal 1481

wex 1704

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ex 1705

This theorem is referenced by: kmlem16 8987

W3C validator