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

Theorem alrimi 2246
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2239. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
alrimi.1 𝑥𝜑
alrimi.2 (𝜑𝜓)
Assertion
Ref Expression
alrimi (𝜑 → ∀𝑥𝜓)

Proof of Theorem alrimi
StepHypRef Expression
1 alrimi.1 . . 3 𝑥𝜑
21nf5ri 2227 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1918 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1650  wnf 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-ex 1875  df-nf 1879
This theorem is referenced by:  nf5d  2294  axc4i  2308  19.12  2330  cbv3v  2335  cbv3  2370  cbv2  2375  sbbidOLD  2494  nfsbd  2536  mo3  2628  eupicka  2659  2moex  2665  2mo  2673  axbnd  2742  abbid  2883  nfcd  2902  ceqsalgALT  3384  ceqsex  3394  vtocldf  3408  elrab3t  3518  morex  3549  sbciedf  3632  csbiebt  3711  csbiedf  3712  ssrd  3766  eqrd  3780  invdisj  4795  zfrepclf  4937  eusv2nf  5030  ssopab2b  5163  imadif  6151  eusvobj1  6836  ssoprab2b  6910  ovmpt2dxf  6984  axrepnd  9669  axunnd  9671  axpownd  9676  axregndlem1  9677  axacndlem1  9682  axacndlem2  9683  axacndlem3  9684  axacndlem4  9685  axacndlem5  9686  axacnd  9687  mreexexd  16576  acsmapd  17446  isch3  28489  ssrelf  29810  eqrelrd2  29811  esumeq12dvaf  30475  bnj1366  31280  bnj571  31356  bnj964  31393  iota5f  31984  bj-hbext  33068  bj-nfext  33070  bj-abbid  33140  wl-mo3t  33715  wl-ax11-lem3  33721  cover2  33863  alrimii  34277  mpt2bi123f  34324  mptbi12f  34328  ss2iundf  38558  pm11.57  39195  pm11.59  39197  tratrb  39346  hbexg  39366  e2ebindALT  39749  mpteq1df  40017  mpteq12da  40026  dvnmul  40728  stoweidlem34  40820  sge0fodjrnlem  41202  preimagelt  41484  preimalegt  41485  pimrecltpos  41491  pimrecltneg  41505  smfaddlem1  41543  smfresal  41567  smfsupmpt  41593  smfinflem  41595  smfinfmpt  41597  ovmpt2rdxf  42718  rspcdf  43025  setrec1lem4  43038
  Copyright terms: Public domain W3C validator