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

Theorem exlimdvv 1870
 Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
exlimdvv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exlimdvv (𝜑 → (∃𝑥𝑦𝜓𝜒))
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥   𝜒,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem exlimdvv
StepHypRef Expression
1 exlimdvv.1 . . 3 (𝜑 → (𝜓𝜒))
21exlimdv 1792 . 2 (𝜑 → (∃𝑦𝜓𝜒))
32exlimdv 1792 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:  euotd  4183  funopg  5164  th3qlem1  6538  fundmen  6707  sbthlemi10  6861  addnq0mo  7278  mulnq0mo  7279  genprndl  7352  genprndu  7353  genpdisj  7354  mullocpr  7402  addsrmo  7574  mulsrmo  7575  cnm  7663  summodc  11183  fsum2dlemstep  11234  prodmodc  11378  txbasval  12473
 Copyright terms: Public domain W3C validator