NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  exlimi Unicode version

Theorem exlimi 1803
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
exlimi.1  F/
exlimi.2
Assertion
Ref Expression
exlimi

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3  F/
2119.23 1801 . 2
3 exlimi.2 . 2
42, 3mpgbi 1549 1
Colors of variables: wff setvar class
Syntax hints:   wi 4  wex 1541   F/wnf 1544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545
This theorem is referenced by:  exlimih  1804  19.41  1879  equs5a  1887  sb5rf  2090  euan  2261  moexex  2273  ceqsex  2893  sbhypf  2904  vtoclgf  2913  vtoclef  2927  copsexg  4607  copsex2g  4609  ralxpf  4827  fv3  5341  tz6.12c  5347
  Copyright terms: Public domain W3C validator