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

Theorem alrimi 2206
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2200. (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 2187 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1817 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1528  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2169
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-nf 1778
This theorem is referenced by:  sbimd  2238  sbbid  2239  nf5d  2286  axc4i  2335  19.12  2340  cbv2OLD  2423  nfsbd  2562  mobid  2632  mo3  2646  eubid  2671  2moexv  2711  eupicka  2718  2moex  2724  2mo  2732  axbndOLD  2797  abbid  2892  nfcd  2973  nfabdw  3005  ceqsalgALT  3536  ceqsex  3546  vtocldf  3561  rspcdf  3614  elrab3t  3683  morex  3714  sbciedf  3817  csbiebt  3916  csbiedf  3917  ssrd  3976  eqrd  3990  invdisj  5047  zfrepclf  5195  eusv2nf  5292  ssopab2bw  5431  ssopab2b  5433  imadif  6437  eusvobj1  7144  ssoprab2b  7217  eqoprab2bw  7218  ovmpodxf  7294  axrepnd  10010  axunnd  10012  axpownd  10017  axregndlem1  10018  axacndlem1  10023  axacndlem2  10024  axacndlem3  10025  axacndlem4  10026  axacndlem5  10027  axacnd  10028  mreexexd  16914  acsmapd  17783  isch3  28951  ssrelf  30300  eqrelrd2  30301  esumeq12dvaf  31195  bnj1366  32006  bnj571  32083  bnj964  32120  iota5f  32858  bj-hbext  33947  bj-nfext  33949  wl-mo3t  34698  wl-ax11-lem3  34705  cover2  34876  alrimii  35284  mpobi123f  35327  mptbi12f  35331  ss2iundf  39888  pm11.57  40605  pm11.59  40607  tratrb  40754  hbexg  40774  e2ebindALT  41147  mpteq1df  41390  mpteq12da  41397  dvnmul  42112  stoweidlem34  42204  sge0fodjrnlem  42583  pimrecltpos  42872  pimrecltneg  42886  smfaddlem1  42924  smfresal  42948  smfsupmpt  42974  smfinflem  42976  smfinfmpt  42978  dfich2OLD  43467  ichnfim  43475  ovmpordxf  44289  setrec1lem4  44695
  Copyright terms: Public domain W3C validator