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

Theorem eximd 1821
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
eximd.1
eximd.2
Assertion
Ref Expression
eximd

Proof of Theorem eximd
StepHypRef Expression
1 eximd.1 . . 3
21nfri 1813 . 2
3 eximd.2 . 2
42, 3eximdh 1641 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1587  F/wnf 1590
This theorem is referenced by:  exlimd  1852  19.41  1911  sbiedOLD  2113  2ax6elem  2166  mo3OLD  2308  moOLD  2314  mopick2  2357  2euex  2362  copsexgOLD  4694  axpowndlem3  8901  axpowndlem3OLD  8902  axregndlem1  8905  axregnd  8907  axregndOLD  8908  spc2ed  26326  finminlem  28973  ssrexf  30195  islpcn  30410  stoweidlem27  30556  stoweidlem34  30563  stoweidlem35  30564  pmapglb2xN  34267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
  Copyright terms: Public domain W3C validator