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

Theorem eximdv 1622
 Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1 (φ → (ψχ))
Assertion
Ref Expression
eximdv (φ → (xψxχ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)

Proof of Theorem eximdv
StepHypRef Expression
1 ax-17 1616 . 2 (φxφ)
2 alimdv.1 . 2 (φ → (ψχ))
31, 2eximdh 1588 1 (φ → (xψxχ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1541 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 This theorem depends on definitions:  df-bi 177  df-ex 1542 This theorem is referenced by:  2eximdv  1624  exlimdv  1636  ax12olem2  1928  moim  2250  morimv  2252  reximdv2  2723  cgsexg  2890  spc3egv  2943  euind  3023  ssel  3267  reupick  3539  reximdva0  3561  uniss  3912  nnpw1ex  4484  coss1  4872  coss2  4873  dmss  4906  dmcosseq  4973  funssres  5144  fv3  5341  dffo4  5423  dffo5  5424  fvclss  5462  mapsn  6026  ncspw1eu  6159  taddc  6229  fnfreclem3  6319
 Copyright terms: Public domain W3C validator