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

Theorem eximdv 1860
 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 1506 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1591 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1472 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  2eximdv  1862  reximdv2  2556  cgsexg  2747  spc3egv  2804  euind  2899  ssel  3122  reupick  3391  reximdva0m  3409  uniss  3793  eusvnfb  4413  coss1  4740  coss2  4741  dmss  4784  dmcosseq  4856  funssres  5211  imain  5251  brprcneu  5460  fv3  5490  dffo4  5614  dffo5  5615  f1eqcocnv  5738  mapsn  6632  ctssdccl  7049  acfun  7136  ccfunen  7178  cc4f  7183  cc4n  7185  dmaddpq  7293  dmmulpq  7294  recexprlemlol  7540  recexprlemupu  7542  ioom  10153  ctinfom  12140  ctinf  12142  omctfn  12155  txcn  12646
 Copyright terms: Public domain W3C validator