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