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

Theorem exlimivv 1819
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 1530 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1530 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-17 1460
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  cgsex2g  2644  cgsex4g  2645  opabss  3862  copsexg  4027  elopab  4041  epelg  4073  0nelelxp  4419  elvvuni  4450  optocl  4462  xpsspw  4498  relopabi  4511  relop  4534  elreldm  4608  xpmlem  4794  dfco2a  4871  unielrel  4895  oprabid  5588  1stval2  5833  2ndval2  5834  xp1st  5843  xp2nd  5844  poxp  5904  rntpos  5926  dftpos4  5932  tpostpos  5933  tfrlem7  5986  th3qlem2  6296  ener  6347  domtr  6353  unen  6382  xpsnen  6386  ltdcnq  6701  archnqq  6721  enq0tr  6738  nqnq0pi  6742  nqnq0  6745  nqpnq0nq  6757  nqnq0a  6758  nqnq0m  6759  nq0m0r  6760  nq0a0  6761  nq02m  6769  prarloc  6807  axaddcl  7146  axmulcl  7148  bj-inex  10965
  Copyright terms: Public domain W3C validator