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

Theorem alrimi 1781
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 1778 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1574 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549   F/wnf 1553
This theorem is referenced by:  nfd  1782  a5i  1807  exlimdOLD  1825  19.12  1869  nfald  1871  nfaldOLD  1872  19.38OLD  1895  equs5eOLD  1911  cbv3  1971  equsalOLD  2000  sbie  2122  sbbid  2152  dvelimdfOLD  2157  sb6rf  2166  nfsbd  2186  eupicka  2344  2moex  2351  axbnd  2415  abbid  2548  nfcd  2566  ralrimi  2779  ceqsalg  2972  ceqsex  2982  vtocldf  2995  morex  3110  sbciedf  3188  csbiebt  3279  csbiedf  3280  ssrd  3345  invdisj  4193  zfrepclf  4318  ssopab2b  4473  eusv2nf  4712  sniota  5436  imadif  5519  ssoprab2b  6122  ovmpt2dxf  6190  eusvobj1  6574  riotasv2dOLD  6586  axrepnd  8458  axunnd  8460  axpownd  8465  axregndlem1  8466  axacndlem1  8471  axacndlem2  8472  axacndlem3  8473  axacndlem4  8474  axacndlem5  8475  axacnd  8476  mreexexd  13861  acsmapd  14592  isch3  22732  esumeq12dvaf  24416  iota5f  25170  cover2  26352  pm11.57  27503  pm11.59  27505  rfcnpre1  27604  rfcnpre2  27616  stoweidlem34  27697  stoweidlem59  27722  tratrb  28475  hbexg  28498  e2ebindALT  28896  bnj1366  29055  bnj571  29131  bnj964  29168  nfaldwAUX7  29306  equsalNEW7  29341  sbbidNEW7  29426  sb6rfNEW7  29441  sb8wAUX7  29442  nfaldOLD7  29529  nfsbdOLD7  29589  dvelimdfOLD7  29590  sb8OLD7  29595
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator