![]() |
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 1841 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 1742 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 19.41.1 |
. . . . 5
![]() ![]() ![]() ![]() | |
3 | 2 | 19.9 1981 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | anbi2i 705 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylib 201 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | pm3.21 454 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 2, 6 | eximd 1971 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7 | impcom 436 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 5, 8 | impbii 192 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-12 1944 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-nf 1679 |
This theorem is referenced by: 19.42 2063 exan 2064 equsexv 2077 eean 2088 eeeanv 2090 equsexALT 2142 2sb5rf 2291 r19.41 2955 eliunxp 4991 dfopab2 6874 dfoprab3s 6875 xpcomco 7688 mpt2mptxf 28329 bnj605 29767 bnj607 29776 2sb5nd 36971 2sb5ndVD 37347 2sb5ndALT 37369 eliunxp2 40388 |
Copyright terms: Public domain | W3C validator |