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

Theorem exlimdv 1792
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
exlimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exlimdv (𝜑 → (∃𝑥𝜓𝜒))
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimdv
StepHypRef Expression
1 ax-17 1507 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-17 1507 . 2 (𝜒 → ∀𝑥𝜒)
3 exlimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3exlimdh 1576 1 (𝜑 → (∃𝑥𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1424  ax-gen 1426  ax-ie2 1471  ax-17 1507
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v2  1793  exlimdvv  1870  exlimddv  1871  tpid3g  3645  sssnm  3688  pwntru  4129  euotd  4183  ralxfr2d  4392  rexxfr2d  4393  releldmb  4783  relelrnb  4784  elres  4862  iss  4872  imain  5212  elunirn  5674  ovmpt4g  5900  oprssdmm  6076  op1steq  6084  fo2ndf  6131  reldmtpos  6157  rntpos  6161  tfrlemibacc  6230  tfrlemibxssdm  6231  tfrlemibfn  6232  tfrexlem  6238  tfr1onlembacc  6246  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfrcllembacc  6259  tfrcllembxssdm  6260  tfrcllembfn  6261  map0g  6589  xpdom3m  6735  phplem4  6756  phpm  6766  findcard2  6790  findcard2s  6791  ac6sfi  6799  fiintim  6824  xpfi  6825  fidcenum  6851  ordiso  6928  ctmlemr  7000  ctm  7001  ctssdc  7005  pm54.43  7062  exmidfodomrlemim  7073  recclnq  7223  ltexnqq  7239  ltbtwnnqq  7246  recexprlemss1l  7466  recexprlemss1u  7467  negm  9433  ioom  10068  seq3f1olemp  10305  fiinfnf1o  10563  fihashf1rn  10566  climcau  11147  summodclem2  11182  zsumdc  11184  isumz  11189  fsumf1o  11190  fisumss  11192  fsumcl2lem  11198  fsumadd  11206  fsummulc2  11248  ntrivcvgap  11348  prodmodclem2  11377  zproddc  11379  ennnfone  11972  enctlem  11979  unct  11989  eltg3  12263  tgtop  12274  tgidm  12280  tgrest  12375  tgcn  12414  xblm  12623  dvfgg  12863  dvcnp2cntop  12869  pwtrufal  13363
  Copyright terms: Public domain W3C validator