Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eximdv Structured version   GIF version

Theorem eximdv 1742
 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 1400 . 2 (φxφ)
2 alimdv.1 . 2 (φ → (ψχ))
31, 2eximdh 1484 1 (φ → (xψxχ))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1362 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  2eximdv  1744  reximdv2  2396  cgsexg  2566  spc3egv  2621  euind  2705  ssel  2916  reupick  3198  reximdva0m  3213  uniss  3575  eusvnfb  4136  coss1  4418  coss2  4419  dmss  4461  dmcosseq  4530  funssres  4868  imain  4907  brprcneu  5096  fv3  5122  dffo4  5240  dffo5  5241  f1eqcocnv  5356  dmaddpq  6238  dmmulpq  6239  recexprlemlol  6460  recexprlemupu  6462
 Copyright terms: Public domain W3C validator