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

Theorem eximdv 1776
 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 1435 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1518 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  2eximdv  1778  reximdv2  2435  cgsexg  2606  spc3egv  2661  euind  2751  ssel  2967  reupick  3249  reximdva0m  3264  uniss  3629  eusvnfb  4214  coss1  4519  coss2  4520  dmss  4562  dmcosseq  4631  funssres  4970  imain  5009  brprcneu  5199  fv3  5225  dffo4  5343  dffo5  5344  f1eqcocnv  5459  dmaddpq  6535  dmmulpq  6536  recexprlemlol  6782  recexprlemupu  6784  ioom  9217
 Copyright terms: Public domain W3C validator