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

Theorem alrimivv 1752
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
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3
21alrimiv 1751 . 2
32alrimiv 1751 1
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1333  ax-gen 1335  ax-17 1416
This theorem is referenced by:  2ax17  1755  euind  2722  sbnfc2  2900  ssopab2dv  4006  suctr  4124  eusvnf  4151  ordsuc  4241  ssrel  4371  relssdv  4375  eqrelrdv  4379  eqbrrdv  4380  eqrelrdv2  4382  ssrelrel  4383  iss  4597  funssres  4885  funun  4887  fununi  4910  fsn  5278  ovg  5581  caovimo  5636  oprabexd  5696  qliftfund  6125  eroveu  6133  th3qlem1  6144  addnq0mo  6429  mulnq0mo  6430  ltexprlemdisj  6579  recexprlemdisj  6601  addsrmo  6651  mulsrmo  6652
  Copyright terms: Public domain W3C validator