Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exim | Structured version Visualization version Unicode version |
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
exim |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 | |
2 | 1 | aleximi 1759 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 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-ex 1705 |
This theorem is referenced by: eximi 1762 19.38b 1768 19.23v 1902 nf5-1 2023 19.8a 2052 19.9ht 2143 spimt 2253 elex2 3216 elex22 3217 vtoclegft 3280 spcimgft 3284 bj-axdd2 32576 bj-2exim 32595 bj-exlimh 32602 bj-alexim 32605 bj-sbex 32626 bj-alequexv 32655 bj-eqs 32663 bj-axc10 32707 bj-alequex 32708 bj-spimtv 32718 bj-spcimdv 32884 bj-spcimdvv 32885 2exim 38578 pm11.71 38597 onfrALTlem2 38761 19.41rg 38766 ax6e2nd 38774 elex2VD 39073 elex22VD 39074 onfrALTlem2VD 39125 19.41rgVD 39138 ax6e2eqVD 39143 ax6e2ndVD 39144 ax6e2ndeqVD 39145 ax6e2ndALT 39166 ax6e2ndeqALT 39167 |
Copyright terms: Public domain | W3C validator |