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

Theorem alrimi 1745
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 1742 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1552 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfd  1746  a5i  1758  nfald  1775  exlimd  1803  19.38  1810  equs5e  1829  equsal  1900  sbbid  2018  dvelimdf  2022  sb6rf  2031  sb8  2032  nfsbd  2050  eupicka  2207  2moex  2214  abbid  2396  nfcd  2414  ralrimi  2624  ceqsalg  2812  ceqsex  2822  vtocldf  2835  morex  2949  sbciedf  3026  csbiebt  3117  csbiedf  3118  invdisj  4012  zfrepclf  4137  ssopab2b  4291  eusv2nf  4532  iota2df  5243  sniota  5246  imadif  5327  ssoprab2b  5905  ovmpt2dxf  5973  eusvobj1  6338  riotasv2dOLD  6350  axrepnd  8216  axunnd  8218  axpownd  8223  axregndlem1  8224  axacndlem1  8229  axacndlem2  8230  axacndlem3  8231  axacndlem4  8232  axacndlem5  8233  axacnd  8234  mreexexd  13550  acsmapd  14281  vitalilem3  18965  isch3  21821  ssrd  23125  esumeq12dvaf  23414  sigaclcuni  23479  imgfldref2  25064  imonclem  25813  ismonc  25814  iepiclem  25823  isepic  25824  cover2  26358  pm11.57  27588  pm11.59  27590  rfcnpre1  27690  rfcnpre2  27702  stoweidlem34  27783  stoweidlem59  27808  tratrb  28299  hbexg  28322  e2ebindALT  28706  bnj1366  28862  bnj571  28938  bnj964  28975
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator