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

Theorem eximdv 1805
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 1462 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1545 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  2eximdv  1807  reximdv2  2468  cgsexg  2648  spc3egv  2703  euind  2793  ssel  3008  reupick  3272  reximdva0m  3287  uniss  3657  eusvnfb  4250  coss1  4559  coss2  4560  dmss  4603  dmcosseq  4672  funssres  5021  imain  5061  brprcneu  5261  fv3  5291  dffo4  5410  dffo5  5411  f1eqcocnv  5531  mapsn  6399  dmaddpq  6882  dmmulpq  6883  recexprlemlol  7129  recexprlemupu  7131  ioom  9600
  Copyright terms: Public domain W3C validator