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

Theorem eximdv 1902
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 1548 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1633 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1514
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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  2eximdv  1904  reximdv2  2604  cgsexg  2806  spc3egv  2864  euind  2959  ssel  3186  reupick  3456  reximdva0m  3475  uniss  3870  eusvnfb  4500  coss1  4832  coss2  4833  dmss  4876  dmcosseq  4949  funssres  5312  imain  5355  brprcneu  5568  fv3  5598  dffo4  5727  dffo5  5728  f1eqcocnv  5859  mapsn  6776  ctssdccl  7212  acfun  7318  ccfunen  7375  cc4f  7380  cc4n  7382  dmaddpq  7491  dmmulpq  7492  recexprlemlol  7738  recexprlemupu  7740  ioom  10401  ctinfom  12770  ctinf  12772  omctfn  12785  nninfdclemp1  12792  ptex  13067  subgintm  13505  txcn  14718
  Copyright terms: Public domain W3C validator