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

Theorem exlimdv 1700
 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 1419 . 2 (𝜑 → ∀𝑥𝜑)
2 ax-17 1419 . 2 (𝜒 → ∀𝑥𝜒)
3 exlimdv.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3exlimdh 1487 1 (𝜑 → (∃𝑥𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1381 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1336  ax-gen 1338  ax-ie2 1383  ax-17 1419 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  ax11v2  1701  exlimdvv  1777  exlimddv  1778  tpid3g  3483  sssnm  3525  euotd  3991  ralxfr2d  4196  rexxfr2d  4197  releldmb  4571  relelrnb  4572  elres  4646  iss  4654  imain  4981  elunirn  5405  ovmpt4g  5623  op1steq  5805  fo2ndf  5848  reldmtpos  5868  rntpos  5872  tfrlemibacc  5940  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrexlem  5948  freccl  5993  xpdom3m  6308  phplem4  6318  phpm  6327  findcard2  6346  findcard2s  6347  ac6sfi  6352  ordiso  6358  recclnq  6490  ltexnqq  6506  ltbtwnnqq  6513  recexprlemss1l  6733  recexprlemss1u  6734  negm  8550  climcau  9866
 Copyright terms: Public domain W3C validator