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

Theorem exlimdv 1716
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 1435 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-17 1435 . 2 (𝜒 → ∀𝑥𝜒)
3 exlimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3exlimdh 1503 1 (𝜑 → (∃𝑥𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-5 1352  ax-gen 1354  ax-ie2 1399  ax-17 1435
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  ax11v2  1717  exlimdvv  1793  exlimddv  1794  tpid3g  3511  sssnm  3553  euotd  4019  ralxfr2d  4224  rexxfr2d  4225  releldmb  4599  relelrnb  4600  elres  4674  iss  4682  imain  5009  elunirn  5433  ovmpt4g  5651  op1steq  5833  fo2ndf  5876  reldmtpos  5899  rntpos  5903  tfrlemibacc  5971  tfrlemibxssdm  5972  tfrlemibfn  5973  tfrexlem  5979  freccl  6024  xpdom3m  6339  phplem4  6349  phpm  6358  findcard2  6377  findcard2s  6378  ac6sfi  6383  ordiso  6416  recclnq  6548  ltexnqq  6564  ltbtwnnqq  6571  recexprlemss1l  6791  recexprlemss1u  6792  negm  8647  ioom  9217  climcau  10097
  Copyright terms: Public domain W3C validator