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  1850  equs5e  1912  aev  1923  sbbid  1970  dvelimdf  1976  sb6rf  1985  sb8  1986  alrimiv  2012  nfsbd  2071  eupicka  2177  2moex  2184  abbid  2362  nfcd  2380  ralrimi  2586  ceqsalg  2750  ceqsex  2760  vtocldf  2773  morex  2886  sbciedf  2956  csbiebt  3045  csbiedf  3046  invdisj  3909  zfrepclf  4034  ssopab2b  4184  eusv2nf  4423  imadif  5184  ssoprab2b  5757  ovmpt2dxf  5825  iota2df  6167  sniota  6170  eusvobj1  6224  riotasv2dOLD  6236  axrepnd  8096  axunnd  8098  axpownd  8103  axregndlem1  8104  axacndlem1  8109  axacndlem2  8110  axacndlem3  8111  axacndlem4  8112  axacndlem5  8113  axacnd  8114  vitalilem3  18797  isch3  21651  imgfldref2  24229  imonclem  24979  ismonc  24980  iepiclem  24989  isepic  24990  cover2  25524  pm11.57  26754  pm11.59  26756  tratrb  26992  hbexg  27015  e2ebindALT  27396  bnj1366  27551  bnj571  27627  bnj964  27664
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