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

Theorem alrimivv 1803
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 1802 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1802 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1381  ax-gen 1383  ax-17 1464
This theorem is referenced by:  2ax17  1806  euind  2800  sbnfc2  2986  exmidel  4025  exmidundif  4026  ssopab2dv  4096  suctr  4239  eusvnf  4266  ordsuc  4369  ssrel  4514  relssdv  4518  eqrelrdv  4522  eqbrrdv  4523  eqrelrdv2  4525  ssrelrel  4526  iss  4745  funssres  5042  funun  5044  fununi  5068  fsn  5453  ovg  5765  caovimo  5820  oprabexd  5880  qliftfund  6355  eroveu  6363  th3qlem1  6374  exmidfodomrlemim  6806  addnq0mo  6985  mulnq0mo  6986  ltexprlemdisj  7144  recexprlemdisj  7168  addsrmo  7268  mulsrmo  7269  isummo  10737  exmidsbth  11571
  Copyright terms: Public domain W3C validator