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

Theorem eximd 1882
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1654. (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 1874 . 2
3 eximd.2 . 2
42, 3eximdh 1673 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612  F/wnf 1616
This theorem is referenced by:  exlimd  1914  19.41  1971  2ax6elem  2193  mo3OLD  2324  mopick2  2362  2euex  2366  reximd2a  2927  copsexgOLD  4738  axpowndlem3  8996  axpowndlem3OLD  8997  axregndlem1  9000  axregnd  9002  axregndOLD  9003  spc2ed  27372  finminlem  30136  ssrexf  31388  islpcn  31645  stoweidlem27  31809  stoweidlem34  31816  stoweidlem35  31817  pmapglb2xN  35496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator