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

Theorem alrimi 1955
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 1987. (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 1952 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1693 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1442   F/wnf 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668
This theorem is referenced by:  nfd  1956  axc4i  1980  19.12  2033  nfald  2034  cbv3v  2059  cbv3  2108  cbv2  2113  sbbid  2232  nfsbd  2271  mo3  2336  eupicka  2366  2moex  2372  2mo  2380  axbnd  2430  abbid  2568  nfcd  2587  ralrimiOLD  2789  ceqsalgALT  3073  ceqsex  3083  vtocldf  3097  elrab3t  3195  morex  3222  sbciedf  3303  csbiebt  3383  csbiedf  3384  ssrd  3437  invdisj  4391  zfrepclf  4521  eusv2nf  4601  ssopab2b  4728  imadif  5658  eusvobj1  6284  ssoprab2b  6348  ovmpt2dxf  6422  axrepnd  9019  axunnd  9021  axpownd  9026  axregndlem1  9027  axacndlem1  9032  axacndlem2  9033  axacndlem3  9034  axacndlem4  9035  axacndlem5  9036  axacnd  9037  mreexexd  15554  acsmapd  16424  isch3  26894  ssrelf  28221  eqrelrd2  28222  esumeq12dvaf  28852  bnj1366  29641  bnj571  29717  bnj964  29754  iota5f  30357  bj-hbext  31304  bj-nfext  31306  bj-cbv3v2  31328  bj-abbid  31393  wl-mo3t  31905  wl-ax11-lem3  31917  cover2  32040  alrimii  32359  mpt2bi123f  32406  mptbi12f  32410  ss2iundf  36251  pm11.57  36739  pm11.59  36741  tratrb  36897  hbexg  36923  e2ebindALT  37326  dvnmul  37818  stoweidlem34  37895  sge0fodjrnlem  38258  ovmpt2rdxf  40173
  Copyright terms: Public domain W3C validator