Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  exim Unicode version

Theorem exim 1573
 Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
exim

Proof of Theorem exim
StepHypRef Expression
1 con3 128 . . . 4
21al2imi 1549 . . 3
3 alnex 1569 . . 3
4 alnex 1569 . . 3
52, 3, 43imtr3g 262 . 2
65con4d 99 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6  wal 1532  wex 1537 This theorem is referenced by:  eximi  1574  exbi  1579  eximdh  1586  19.29  1595  19.25  1602  19.30  1603  ax12o10lem14  1648  19.23t  1776  2mo  2191  elex22  2738  elex2  2739  vtoclegft  2793  cla4imgft  2797  ssoprab2  5756  2exim  26743  pm11.71  26762  onfrALTlem2  27004  19.41rg  27009  a9e2nd  27017  elex2VD  27304  elex22VD  27305  onfrALTlem2VD  27355  19.41rgVD  27368  a9e2eqVD  27373  a9e2ndVD  27374  a9e2ndeqVD  27375  a9e2ndALT  27397  a9e2ndeqALT  27398 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536 This theorem depends on definitions:  df-bi 179  df-ex 1538
 Copyright terms: Public domain W3C validator