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

Theorem exlimivv 1868
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
Hypothesis
Ref Expression
exlimivv.1 (𝜑𝜓)
Assertion
Ref Expression
exlimivv (∃𝑥𝑦𝜑𝜓)
Distinct variable groups:   𝜓,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3 (𝜑𝜓)
21exlimiv 1577 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1577 1 (∃𝑥𝑦𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470  ax-17 1506 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  cgsex2g  2722  cgsex4g  2723  opabss  3992  copsexg  4166  elopab  4180  epelg  4212  0nelelxp  4568  elvvuni  4603  optocl  4615  xpsspw  4651  relopabi  4665  relop  4689  elreldm  4765  xpmlem  4959  dfco2a  5039  unielrel  5066  oprabid  5803  1stval2  6053  2ndval2  6054  xp1st  6063  xp2nd  6064  poxp  6129  rntpos  6154  dftpos4  6160  tpostpos  6161  tfrlem7  6214  th3qlem2  6532  ener  6673  domtr  6679  unen  6710  xpsnen  6715  mapen  6740  ltdcnq  7217  archnqq  7237  enq0tr  7254  nqnq0pi  7258  nqnq0  7261  nqpnq0nq  7273  nqnq0a  7274  nqnq0m  7275  nq0m0r  7276  nq0a0  7277  nq02m  7285  prarloc  7323  axaddcl  7684  axmulcl  7686  hashfacen  10591  bj-inex  13164
 Copyright terms: Public domain W3C validator