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

Theorem alrimivv 1733
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1 (φψ)
Assertion
Ref Expression
alrimivv (φxyψ)
Distinct variable groups:   φ,x   φ,y
Allowed substitution hints:   ψ(x,y)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3 (φψ)
21alrimiv 1732 . 2 (φyψ)
32alrimiv 1732 1 (φxyψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1224
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1312  ax-gen 1314  ax-17 1396
This theorem is referenced by:  2ax17  1736  euind  2701  sbnfc2  2879  ssopab2dv  3985  suctrALT  4103  suctr  4104  eusvnf  4131  ordsuc  4221  ssrel  4351  relssdv  4355  eqrelrdv  4359  eqbrrdv  4360  eqrelrdv2  4362  ssrelrel  4363  iss  4577  funssres  4864  funun  4866  fununi  4889  fsn  5256  ovg  5558  caovimo  5613  oprabexd  5673  qliftfund  6096  eroveu  6104  th3qlem1  6115  addnq0mo  6296  mulnq0mo  6297  ltexprlemdisj  6437  recexprlemdisj  6458  addsrmo  6487  mulsrmo  6488
  Copyright terms: Public domain W3C validator