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

Theorem alrimi 1882
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 1910. (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 1879 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1647 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1396   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  nfd  1883  axc4i  1903  19.12  1955  nfald  1956  cbv3  2020  cbv2  2025  sbbid  2146  nfsbd  2188  mo3  2324  eupicka  2356  2moex  2362  2mo  2370  2moOLD  2371  axbnd  2431  abbid  2589  nfcd  2610  ralrimiOLD  2855  ceqsalgALT  3132  ceqsex  3142  vtocldf  3155  elrab3t  3253  morex  3280  sbciedf  3360  csbiebt  3440  csbiedf  3441  ssrd  3494  invdisj  4428  zfrepclf  4556  eusv2nf  4635  ssopab2b  4763  imadif  5645  eusvobj1  6264  ssoprab2b  6327  ovmpt2dxf  6401  axrepnd  8960  axunnd  8962  axpownd  8967  axregndlem1  8968  axacndlem1  8974  axacndlem2  8975  axacndlem3  8976  axacndlem4  8977  axacndlem5  8978  axacnd  8979  mreexexd  15137  acsmapd  16007  isch3  26357  ssrelf  27681  eqrelrd2  27682  esumeq12dvaf  28260  iota5f  29343  wl-mo3t  30261  wl-ax11-lem3  30267  cover2  30444  alrimii  30764  mpt2bi123f  30811  mptbi12f  30815  pm11.57  31536  pm11.59  31538  dvnmul  31979  stoweidlem34  32055  ovmpt2rdxf  33182  tratrb  33697  hbexg  33723  e2ebindALT  34130  bnj1366  34289  bnj571  34365  bnj964  34402  bj-hbext  34665  bj-nfext  34667  bj-cbv3v  34689  bj-cbv3v2  34690  bj-abbid  34765
  Copyright terms: Public domain W3C validator