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

Theorem alrimi 1749
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 1746 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1557 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532   F/wnf 1536
This theorem is referenced by:  nfd  1750  a5i  1762  nfald  1779  exlimd  1807  19.38  1814  equs5e  1838  equsal  1904  aev  1957  sbbid  1992  dvelimdf  1998  sb6rf  2007  sb8  2008  nfsbd  2048  eupicka  2208  2moex  2215  abbid  2397  nfcd  2415  ralrimi  2625  ceqsalg  2813  ceqsex  2823  vtocldf  2836  morex  2950  sbciedf  3027  csbiebt  3118  csbiedf  3119  invdisj  4013  zfrepclf  4138  ssopab2b  4290  eusv2nf  4531  imadif  5292  ssoprab2b  5866  ovmpt2dxf  5934  iota2df  6276  sniota  6279  eusvobj1  6333  riotasv2dOLD  6345  axrepnd  8211  axunnd  8213  axpownd  8218  axregndlem1  8219  axacndlem1  8224  axacndlem2  8225  axacndlem3  8226  axacndlem4  8227  axacndlem5  8228  axacnd  8229  mreexexd  13544  acsmapd  14275  vitalilem3  18959  isch3  21813  imgfldref2  24462  imonclem  25212  ismonc  25213  iepiclem  25222  isepic  25223  cover2  25757  pm11.57  26987  pm11.59  26989  rfcnpre1  27089  rfcnpre2  27101  stoweidlem34  27182  stoweidlem59  27207  tratrb  27570  hbexg  27593  e2ebindALT  27974  bnj1366  28129  bnj571  28205  bnj964  28242
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-nf 1537
  Copyright terms: Public domain W3C validator