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

Theorem exlimdv 1744
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 1462 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-17 1462 . 2 (𝜒 → ∀𝑥𝜒)
3 exlimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3exlimdh 1530 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-5 1379  ax-gen 1381  ax-ie2 1426  ax-17 1462
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ax11v2  1745  exlimdvv  1822  exlimddv  1823  tpid3g  3537  sssnm  3580  euotd  4053  ralxfr2d  4258  rexxfr2d  4259  releldmb  4638  relelrnb  4639  elres  4713  iss  4723  imain  5057  elunirn  5499  ovmpt4g  5717  op1steq  5899  fo2ndf  5942  reldmtpos  5965  rntpos  5969  tfrlemibacc  6038  tfrlemibxssdm  6039  tfrlemibfn  6040  tfrexlem  6046  tfr1onlembacc  6054  tfr1onlembxssdm  6055  tfr1onlembfn  6056  tfrcllembacc  6067  tfrcllembxssdm  6068  tfrcllembfn  6069  map0g  6390  xpdom3m  6495  phplem4  6516  phpm  6526  findcard2  6550  findcard2s  6551  ac6sfi  6559  xpfi  6583  ordiso  6665  pm54.43  6754  exmidfodomrlemim  6763  recclnq  6887  ltexnqq  6903  ltbtwnnqq  6910  recexprlemss1l  7130  recexprlemss1u  7131  negm  9024  ioom  9592  iseqf1olemp  9827  fiinfnf1o  10082  fihashf1rn  10085  climcau  10618  isummolem2  10653  zisum  10655  isumz  10659  fsumf1o  10660
  Copyright terms: Public domain W3C validator