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

Theorem alrimivv 1797
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimivv  |-  ( ph  ->  A. x A. y ps )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3  |-  ( ph  ->  ps )
21alrimiv 1796 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1796 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1377  ax-gen 1379  ax-17 1460
This theorem is referenced by:  2ax17  1800  euind  2780  sbnfc2  2963  ssopab2dv  4041  suctr  4184  eusvnf  4211  ordsuc  4314  ssrel  4454  relssdv  4458  eqrelrdv  4462  eqbrrdv  4463  eqrelrdv2  4465  ssrelrel  4466  iss  4684  funssres  4972  funun  4974  fununi  4998  fsn  5367  ovg  5670  caovimo  5725  oprabexd  5785  qliftfund  6255  eroveu  6263  th3qlem1  6274  addnq0mo  6699  mulnq0mo  6700  ltexprlemdisj  6858  recexprlemdisj  6882  addsrmo  6982  mulsrmo  6983
  Copyright terms: Public domain W3C validator