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

Theorem alrimivv 1847
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 1846 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1846 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1423  ax-gen 1425  ax-17 1506
This theorem is referenced by:  2ax17  1850  euind  2866  sbnfc2  3055  exmidsssn  4120  exmidel  4123  exmidundif  4124  exmidundifim  4125  ssopab2dv  4195  suctr  4338  eusvnf  4369  ordsuc  4473  ssrel  4622  relssdv  4626  eqrelrdv  4630  eqbrrdv  4631  eqrelrdv2  4633  ssrelrel  4634  iss  4860  funssres  5160  funun  5162  fununi  5186  fsn  5585  ovg  5902  caovimo  5957  oprabexd  6018  qliftfund  6505  eroveu  6513  th3qlem1  6524  exmidfodomrlemim  7050  addnq0mo  7248  mulnq0mo  7249  ltexprlemdisj  7407  recexprlemdisj  7431  addsrmo  7544  mulsrmo  7545  summodc  11145  limcimo  12788  exmidsbth  13204
  Copyright terms: Public domain W3C validator