New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  exlimi GIF 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 xψ
exlimi.2 (φψ)
Assertion
Ref Expression
exlimi (xφψ)

Proof of Theorem exlimi
StepHypRef Expression
1 exlimi.1 . . 3 xψ
2119.23 1801 . 2 (x(φψ) ↔ (xφψ))
3 exlimi.2 . 2 (φψ)
42, 3mpgbi 1549 1 (xφψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1541  Ⅎ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