MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alrimi Unicode version

Theorem alrimi 1706
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
alrimi.1  |-  F/ x ph
alrimi.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimi  |-  ( ph  ->  A. x ps )

Proof of Theorem alrimi
StepHypRef Expression
1 alrimi.1 . . 3  |-  F/ x ph
21nfri 1703 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1553 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532   F/wnf 1539
This theorem is referenced by:  nfd  1707  a5i  1721  nfald  1742  19.12  1766  exlimd  1784  19.38  1791  equsal  1851  equs5e  1913  aev  1924  sbbid  1971  dvelimdf  1977  sb6rf  1986  sb8  1987  alrimiv  2013  nfsbd  2074  eupicka  2180  2moex  2187  abbid  2369  nfcd  2387  ralrimi  2597  ceqsalg  2780  ceqsex  2790  vtocldf  2803  morex  2917  sbciedf  2987  csbiebt  3078  csbiedf  3079  invdisj  3972  zfrepclf  4097  ssopab2b  4249  eusv2nf  4490  imadif  5251  ssoprab2b  5825  ovmpt2dxf  5893  iota2df  6235  sniota  6238  eusvobj1  6292  riotasv2dOLD  6304  axrepnd  8170  axunnd  8172  axpownd  8177  axregndlem1  8178  axacndlem1  8183  axacndlem2  8184  axacndlem3  8185  axacndlem4  8186  axacndlem5  8187  axacnd  8188  mreexexd  13498  acsmapd  14229  vitalilem3  18913  isch3  21767  imgfldref2  24416  imonclem  25166  ismonc  25167  iepiclem  25176  isepic  25177  cover2  25711  pm11.57  26941  pm11.59  26943  rfcnpre1  27044  rfcnpre2  27056  stoweidlem34  27104  stoweidlem59  27129  tratrb  27336  hbexg  27359  e2ebindALT  27740  bnj1366  27895  bnj571  27971  bnj964  28008
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540
  Copyright terms: Public domain W3C validator