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

Theorem exlimdv 1758
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 1474 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-17 1474 . 2 (𝜒 → ∀𝑥𝜒)
3 exlimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3exlimdh 1543 1 (𝜑 → (∃𝑥𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-5 1391  ax-gen 1393  ax-ie2 1438  ax-17 1474
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v2  1759  exlimdvv  1836  exlimddv  1837  tpid3g  3585  sssnm  3628  euotd  4114  ralxfr2d  4323  rexxfr2d  4324  releldmb  4714  relelrnb  4715  elres  4791  iss  4801  imain  5141  elunirn  5599  ovmpt4g  5825  op1steq  6007  fo2ndf  6054  reldmtpos  6080  rntpos  6084  tfrlemibacc  6153  tfrlemibxssdm  6154  tfrlemibfn  6155  tfrexlem  6161  tfr1onlembacc  6169  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfrcllembacc  6182  tfrcllembxssdm  6183  tfrcllembfn  6184  map0g  6512  xpdom3m  6657  phplem4  6678  phpm  6688  findcard2  6712  findcard2s  6713  ac6sfi  6721  fiintim  6746  xpfi  6747  fidcenum  6772  ordiso  6836  ctmlemr  6908  ctm  6909  ctssdc  6912  pm54.43  6957  exmidfodomrlemim  6966  recclnq  7101  ltexnqq  7117  ltbtwnnqq  7124  recexprlemss1l  7344  recexprlemss1u  7345  negm  9257  ioom  9879  seq3f1olemp  10116  fiinfnf1o  10373  fihashf1rn  10376  climcau  10955  summodclem2  10990  zsumdc  10992  isumz  10997  fsumf1o  10998  fisumss  11000  fsumcl2lem  11006  fsumadd  11014  fsummulc2  11056  ennnfone  11730  eltg3  12008  tgtop  12019  tgidm  12025  tgrest  12120  tgcn  12158  xblm  12345  dvfgg  12530  pwtrufal  12777  pwntru  12778
  Copyright terms: Public domain W3C validator