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

Theorem alrimi 1757
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 1754 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1555 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfd  1758  a5i  1770  nfald  1787  exlimd  1815  19.38  1822  equs5e  1841  equsal  1913  sbbid  2031  dvelimdf  2035  sb6rf  2044  sb8  2045  nfsbd  2063  eupicka  2220  2moex  2227  abbid  2409  nfcd  2427  ralrimi  2637  ceqsalg  2825  ceqsex  2835  vtocldf  2848  morex  2962  sbciedf  3039  csbiebt  3130  csbiedf  3131  invdisj  4028  zfrepclf  4153  ssopab2b  4307  eusv2nf  4548  iota2df  5259  sniota  5262  imadif  5343  ssoprab2b  5921  ovmpt2dxf  5989  eusvobj1  6354  riotasv2dOLD  6366  axrepnd  8232  axunnd  8234  axpownd  8239  axregndlem1  8240  axacndlem1  8245  axacndlem2  8246  axacndlem3  8247  axacndlem4  8248  axacndlem5  8249  axacnd  8250  mreexexd  13566  acsmapd  14297  vitalilem3  18981  isch3  21837  ssrd  23141  esumeq12dvaf  23429  sigaclcuni  23494  imgfldref2  25167  imonclem  25916  ismonc  25917  iepiclem  25926  isepic  25927  cover2  26461  pm11.57  27691  pm11.59  27693  rfcnpre1  27793  rfcnpre2  27805  stoweidlem34  27886  stoweidlem59  27911  tratrb  28598  hbexg  28621  e2ebindALT  29022  bnj1366  29178  bnj571  29254  bnj964  29291  nfaldwAUX7  29429  equsalNEW7  29464  sbbidNEW7  29549  sb6rfNEW7  29564  sb8wAUX7  29565  ax7w3AUX7  29621  nfaldOLD7  29644  nfsbdOLD7  29704  dvelimdfOLD7  29705  sb8OLD7  29710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator