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

Theorem alrimi 2204
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2198. (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 2185 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1815 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-nf 1776
This theorem is referenced by:  sbimd  2236  sbbid  2237  nf5d  2284  axc4i  2333  19.12  2338  cbv2OLD  2421  nfsbd  2560  mobid  2630  mo3  2644  eubid  2669  2moexv  2708  eupicka  2715  2moex  2721  2mo  2729  axbndOLD  2792  abbid  2887  nfcd  2968  nfabdw  3000  ceqsalgALT  3531  ceqsex  3541  vtocldf  3556  rspcdf  3609  elrab3t  3678  morex  3709  sbciedf  3812  csbiebt  3911  csbiedf  3912  ssrd  3971  eqrd  3985  invdisj  5042  zfrepclf  5190  eusv2nf  5287  ssopab2bw  5426  ssopab2b  5428  imadif  6432  eusvobj1  7139  ssoprab2b  7212  eqoprab2bw  7213  ovmpodxf  7289  axrepnd  10005  axunnd  10007  axpownd  10012  axregndlem1  10013  axacndlem1  10018  axacndlem2  10019  axacndlem3  10020  axacndlem4  10021  axacndlem5  10022  axacnd  10023  mreexexd  16909  acsmapd  17778  isch3  28946  ssrelf  30295  eqrelrd2  30296  esumeq12dvaf  31190  bnj1366  32001  bnj571  32078  bnj964  32115  iota5f  32853  bj-hbext  33942  bj-nfext  33944  wl-mo3t  34694  wl-ax11-lem3  34701  cover2  34872  alrimii  35280  mpobi123f  35323  mptbi12f  35327  ss2iundf  39884  pm11.57  40601  pm11.59  40603  tratrb  40750  hbexg  40770  e2ebindALT  41143  mpteq1df  41386  mpteq12da  41393  dvnmul  42108  stoweidlem34  42200  sge0fodjrnlem  42579  pimrecltpos  42868  pimrecltneg  42882  smfaddlem1  42920  smfresal  42944  smfsupmpt  42970  smfinflem  42972  smfinfmpt  42974  dfich2OLD  43463  ichnfim  43471  ovmpordxf  44285  setrec1lem4  44691
  Copyright terms: Public domain W3C validator