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

Theorem alrimi 1929
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 1961. (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 1926 . 2  |-  ( ph  ->  A. x ph )
3 alrimi.2 . 2  |-  ( ph  ->  ps )
42, 3alrimih 1690 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1436   F/wnf 1664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-12 1906
This theorem depends on definitions:  df-bi 189  df-ex 1661  df-nf 1665
This theorem is referenced by:  nfd  1930  axc4i  1954  19.12  2007  nfald  2008  cbv3  2070  cbv2  2075  sbbid  2198  nfsbd  2238  mo3  2304  eupicka  2334  2moex  2340  2mo  2348  2moOLD  2349  axbnd  2400  abbid  2558  nfcd  2579  ralrimiOLD  2827  ceqsalgALT  3108  ceqsex  3118  vtocldf  3131  elrab3t  3229  morex  3256  sbciedf  3336  csbiebt  3416  csbiedf  3417  ssrd  3470  invdisj  4410  zfrepclf  4540  eusv2nf  4620  ssopab2b  4745  imadif  5674  eusvobj1  6297  ssoprab2b  6360  ovmpt2dxf  6434  axrepnd  9021  axunnd  9023  axpownd  9028  axregndlem1  9029  axacndlem1  9034  axacndlem2  9035  axacndlem3  9036  axacndlem4  9037  axacndlem5  9038  axacnd  9039  mreexexd  15547  acsmapd  16417  isch3  26886  ssrelf  28217  eqrelrd2  28218  esumeq12dvaf  28854  bnj1366  29643  bnj571  29719  bnj964  29756  iota5f  30359  bj-hbext  31258  bj-nfext  31260  bj-cbv3v  31282  bj-cbv3v2  31283  bj-abbid  31357  wl-mo3t  31863  wl-ax11-lem3  31875  cover2  31998  alrimii  32317  mpt2bi123f  32364  mptbi12f  32368  ss2iundf  36155  pm11.57  36641  pm11.59  36643  tratrb  36799  hbexg  36825  e2ebindALT  37231  dvnmul  37682  stoweidlem34  37759  sge0fodjrnlem  38090  ovmpt2rdxf  39464
  Copyright terms: Public domain W3C validator