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

Theorem exlimivv 1773
 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 (xyφψ)
Distinct variable groups:   ψ,x   ψ,y
Allowed substitution hints:   φ(x,y)

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3 (φψ)
21exlimiv 1486 . 2 (yφψ)
32exlimiv 1486 1 (xyφψ)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1378 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1335  ax-ie2 1380  ax-17 1416 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  cgsex2g  2584  cgsex4g  2585  opabss  3812  copsexg  3972  elopab  3986  epelg  4018  0nelelxp  4316  elvvuni  4347  optocl  4359  xpsspw  4393  relopabi  4406  relop  4429  elreldm  4503  xpmlem  4687  dfco2a  4764  unielrel  4788  oprabid  5480  1stval2  5724  2ndval2  5725  xp1st  5734  xp2nd  5735  poxp  5794  rntpos  5813  dftpos4  5819  tpostpos  5820  tfrlem7  5874  th3qlem2  6145  ener  6195  domtr  6201  unen  6229  xpsnen  6231  ltdcnq  6381  archnqq  6400  enq0tr  6417  nqnq0pi  6421  nqnq0  6424  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  nq0a0  6440  nq02m  6448  prarloc  6486  axaddcl  6750  axmulcl  6752  bj-inex  9362
 Copyright terms: Public domain W3C validator