![]() |
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 1633 | . . 3 |
3 | simpr 461 | . . . 4 | |
4 | 3 | alimi 1633 | . . 3 |
5 | 2, 4 | jca 532 | . 2 |
6 | id 22 | . . 3 | |
7 | 6 | alanimi 1637 | . 2 |
8 | 5, 7 | impbii 188 | 1 |
Colors of variables: wff setvar class |
Syntax hints: <-> wb 184 /\ wa 369
A. wal 1393 |
This theorem is referenced by: 19.26-2 1681 19.26-3an 1682 19.35OLD 1688 19.43OLD 1694 albiim 1699 2albiim 1700 19.27v 1766 19.28v 1767 19.27 1923 19.28 1924 ax12eq 2271 ax12el 2272 2eu4OLD 2381 bm1.1OLD 2441 r19.26m 2987 unss 3677 ralunb 3684 ssin 3719 intun 4319 intpr 4320 eqrelrel 5109 relop 5158 eqoprab2b 6355 dfer2 7331 axgroth4 9231 grothprim 9233 caubnd 13191 wl-alanbii 30018 dford4 30971 alimp-no-surprise 33196 bj-gl4lem 34183 bj-gl4 34184 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 |
This theorem depends on definitions: df-bi 185 df-an 371 |
Copyright terms: Public domain | W3C validator |