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

Theorem eximdv 1880
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 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem eximdv
StepHypRef Expression
1 ax-17 1526 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1611 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  2eximdv  1882  reximdv2  2576  cgsexg  2772  spc3egv  2829  euind  2924  ssel  3149  reupick  3419  reximdva0m  3438  uniss  3830  eusvnfb  4454  coss1  4782  coss2  4783  dmss  4826  dmcosseq  4898  funssres  5258  imain  5298  brprcneu  5508  fv3  5538  dffo4  5664  dffo5  5665  f1eqcocnv  5791  mapsn  6689  ctssdccl  7109  acfun  7205  ccfunen  7262  cc4f  7267  cc4n  7269  dmaddpq  7377  dmmulpq  7378  recexprlemlol  7624  recexprlemupu  7626  ioom  10260  ctinfom  12428  ctinf  12430  omctfn  12443  nninfdclemp1  12450  ptex  12712  subgintm  13056  txcn  13745
  Copyright terms: Public domain W3C validator