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

Theorem alrimi 1825
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 1822 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1622 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  nfd  1826  axc4i  1846  19.12  1897  nfald  1898  cbv3  1984  sbbid  2118  sb6rfOLD  2146  nfsbd  2170  mo3  2320  eupicka  2365  2moex  2374  2mo  2382  2moOLD  2383  axbnd  2444  abbid  2602  nfcd  2623  ralrimiOLD  2865  ceqsalgALT  3139  ceqsex  3149  vtocldf  3162  elrab3t  3260  morex  3287  sbciedf  3367  csbiebt  3455  csbiedf  3456  ssrd  3509  invdisj  4436  zfrepclf  4564  eusv2nf  4645  ssopab2b  4774  sniota  5577  imadif  5662  eusvobj1  6277  ssoprab2b  6337  ovmpt2dxf  6411  axrepnd  8968  axunnd  8970  axpownd  8977  axregndlem1  8978  axacndlem1  8984  axacndlem2  8985  axacndlem3  8986  axacndlem4  8987  axacndlem5  8988  axacnd  8989  mreexexd  14902  acsmapd  15664  tgldim0eq  23638  isch3  25851  ssrelf  27155  eqrelrd2  27156  esumeq12dvaf  27700  iota5f  28593  wl-mo3t  29614  wl-ax11-lem3  29620  cover2  29823  alrimii  30143  mpt2bi123f  30191  mptbi12f  30195  pm11.57  30889  pm11.59  30891  rfcnpre1  30988  rfcnpre2  31000  iccshift  31138  iooshift  31142  icccncfext  31242  fperdvper  31264  itgiccshift  31314  itgperiod  31315  stoweidlem34  31350  fourierdlem81  31504  ovmpt2rdxf  32012  tratrb  32395  hbexg  32418  e2ebindALT  32818  bnj1366  32976  bnj571  33052  bnj964  33089  bj-hbext  33355  bj-nfext  33357  bj-cbv3v  33379  bj-cbv3v2  33380  bj-abbid  33454
  Copyright terms: Public domain W3C validator