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

Theorem exlimdv 1636
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.)
Hypothesis
Ref Expression
exlimdv.1 (φ → (ψχ))
Assertion
Ref Expression
exlimdv (φ → (xψχ))
Distinct variable groups:   χ,x   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem exlimdv
StepHypRef Expression
1 exlimdv.1 . . 3 (φ → (ψχ))
21eximdv 1622 . 2 (φ → (xψxχ))
3 ax17e 1618 . 2 (xχχ)
42, 3syl6 29 1 (φ → (xψχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1541
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  exlimdvv  1637  exlimddv  1638  ax10  1944  ax11v2  1992  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  tpid3g  3831  sssn  3864  eqpw1uni  4330  nndisjeq  4429  prepeano4  4451  tfindi  4496  tfinsuc  4498  sfintfin  4532  sfinltfin  4535  vfintle  4546  vfinspsslem1  4550  nulnnn  4556  iss  5000  ovmpt4g  5710  erref  5959  erdisj  5972  enpw1  6062  enprmaplem3  6078  enprmaplem6  6081  nenpw1pwlem2  6085  ncdisjun  6136  peano4nc  6150  ncssfin  6151  nntccl  6170  ce0addcnnul  6179  ce0nnulb  6182  fce  6188  dflec3  6221  nclenc  6222  taddc  6228  addcdi  6249  dmfrec  6314  fnfreclem3  6317
  Copyright terms: Public domain W3C validator