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

Theorem alrimi 1811
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 1808 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1612 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1367   F/wnf 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590
This theorem is referenced by:  nfd  1812  axc4i  1832  19.12  1876  nfald  1877  cbv3  1959  sbbid  2095  sb6rfOLD  2123  nfsbd  2148  mo3  2298  eupicka  2343  2moex  2352  2mo  2360  2moOLD  2361  axbnd  2422  abbid  2556  nfcd  2574  ralrimi  2797  ceqsalgALT  2998  ceqsex  3008  vtocldf  3021  elrab3t  3116  morex  3143  sbciedf  3222  csbiebt  3308  csbiedf  3309  ssrd  3361  invdisj  4281  zfrepclf  4409  eusv2nf  4490  ssopab2b  4615  sniota  5408  imadif  5493  eusvobj1  6085  ssoprab2b  6143  ovmpt2dxf  6216  axrepnd  8758  axunnd  8760  axpownd  8767  axregndlem1  8768  axacndlem1  8774  axacndlem2  8775  axacndlem3  8776  axacndlem4  8777  axacndlem5  8778  axacnd  8779  mreexexd  14586  acsmapd  15348  tgldim0eq  22956  isch3  24644  ssrelf  25945  eqrelrd2  25946  esumeq12dvaf  26487  iota5f  27381  wl-mo3t  28397  wl-ax11-lem3  28403  cover2  28607  alrimii  28927  mpt2bi123f  28975  mptbi12f  28979  pm11.57  29642  pm11.59  29644  rfcnpre1  29741  rfcnpre2  29753  stoweidlem34  29829  ovmpt2rdxf  30729  tratrb  31242  hbexg  31265  e2ebindALT  31665  bnj1366  31823  bnj571  31899  bnj964  31936  bj-hbext  32200  bj-nfext  32202  bj-cbv3v  32224  bj-cbv3v2  32225  bj-abbid  32299
  Copyright terms: Public domain W3C validator