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

Theorem eximdv 1760
 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 1419 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1502 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1381 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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  2eximdv  1762  reximdv2  2418  cgsexg  2589  spc3egv  2644  euind  2728  ssel  2939  reupick  3221  reximdva0m  3236  uniss  3601  eusvnfb  4186  coss1  4491  coss2  4492  dmss  4534  dmcosseq  4603  funssres  4942  imain  4981  brprcneu  5171  fv3  5197  dffo4  5315  dffo5  5316  f1eqcocnv  5431  dmaddpq  6477  dmmulpq  6478  recexprlemlol  6724  recexprlemupu  6726
 Copyright terms: Public domain W3C validator