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  2595  ceqsalg  2763  ceqsex  2773  vtocldf  2786  morex  2900  sbciedf  2970  csbiebt  3059  csbiedf  3060  invdisj  3952  zfrepclf  4077  ssopab2b  4228  eusv2nf  4469  imadif  5230  ssoprab2b  5804  ovmpt2dxf  5872  iota2df  6214  sniota  6217  eusvobj1  6271  riotasv2dOLD  6283  axrepnd  8149  axunnd  8151  axpownd  8156  axregndlem1  8157  axacndlem1  8162  axacndlem2  8163  axacndlem3  8164  axacndlem4  8165  axacndlem5  8166  axacnd  8167  mreexexd  13477  acsmapd  14208  vitalilem3  18892  isch3  21746  imgfldref2  24395  imonclem  25145  ismonc  25146  iepiclem  25155  isepic  25156  cover2  25690  pm11.57  26920  pm11.59  26922  rfcnpre1  27023  rfcnpre2  27035  stoweidlem34  27083  stoweidlem59  27108  tratrb  27315  hbexg  27338  e2ebindALT  27719  bnj1366  27874  bnj571  27950  bnj964  27987
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