Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 19.41 | Structured version Visualization version Unicode version |
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1914 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.) |
Ref | Expression |
---|---|
19.41.1 |
Ref | Expression |
---|---|
19.41 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.40 1797 | . . 3 | |
2 | 19.41.1 | . . . . 5 | |
3 | 2 | 19.9 2072 | . . . 4 |
4 | 3 | anbi2i 730 | . . 3 |
5 | 1, 4 | sylib 208 | . 2 |
6 | pm3.21 464 | . . . 4 | |
7 | 2, 6 | eximd 2085 | . . 3 |
8 | 7 | impcom 446 | . 2 |
9 | 5, 8 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 wex 1704 wnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-nf 1710 |
This theorem is referenced by: 19.42 2105 equsexv 2109 exanOLDOLD 2169 eean 2181 eeeanv 2183 equsexALT 2293 2sb5rf 2451 r19.41 3090 eliunxp 5259 dfopab2 7222 dfoprab3s 7223 xpcomco 8050 mpt2mptxf 29477 bnj605 30977 bnj607 30986 2sb5nd 38776 2sb5ndVD 39146 2sb5ndALT 39168 eliunxp2 42112 |
Copyright terms: Public domain | W3C validator |