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

Theorem eximdv 1757
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 1416 . 2 (φxφ)
2 alimdv.1 . 2 (φ → (ψχ))
31, 2eximdh 1499 1 (φ → (xψxχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1378
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  2eximdv  1759  reximdv2  2412  cgsexg  2583  spc3egv  2638  euind  2722  ssel  2933  reupick  3215  reximdva0m  3230  uniss  3592  eusvnfb  4152  coss1  4434  coss2  4435  dmss  4477  dmcosseq  4546  funssres  4885  imain  4924  brprcneu  5114  fv3  5140  dffo4  5258  dffo5  5259  f1eqcocnv  5374  dmaddpq  6363  dmmulpq  6364  recexprlemlol  6596  recexprlemupu  6598
  Copyright terms: Public domain W3C validator