![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 19.26 | Unicode version |
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
19.26 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 457 | . . . 4 | |
2 | 1 | alimi 1605 | . . 3 |
3 | simpr 461 | . . . 4 | |
4 | 3 | alimi 1605 | . . 3 |
5 | 2, 4 | jca 532 | . 2 |
6 | id 22 | . . 3 | |
7 | 6 | alanimi 1608 | . 2 |
8 | 5, 7 | impbii 188 | 1 |
Colors of variables: wff setvar class |
Syntax hints: <-> wb 184 /\ wa 369
A. wal 1368 |
This theorem is referenced by: 19.26-2 1649 19.26-3an 1650 19.35OLD 1656 19.43OLD 1662 albiim 1666 2albiim 1667 19.27 1857 19.28 1858 ax12eq 2248 ax12el 2249 2eu4OLD 2375 bm1.1OLD 2434 r19.26m 2932 unss 3612 ralunb 3619 ssin 3654 intun 4242 intpr 4243 eqrelrel 5023 relop 5072 eqoprab2b 6227 dfer2 7186 axgroth4 9084 grothprim 9086 caubnd 12932 wl-alanbii 28516 dford4 29500 alimp-no-surprise 31414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 |
This theorem depends on definitions: df-bi 185 df-an 371 |
Copyright terms: Public domain | W3C validator |