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

Theorem alrimi 2081
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2074. (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 2064 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1750 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1480  wnf 1707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-12 2046
This theorem depends on definitions:  df-bi 197  df-ex 1704  df-nf 1709
This theorem is referenced by:  nf5d  2117  axc4i  2130  19.12  2163  nfaldOLD  2165  cbv3v  2171  cbv3  2264  cbv2  2269  sbbid  2402  nfsbd  2441  mo3  2506  eupicka  2536  2moex  2542  2mo  2550  axbnd  2600  abbid  2739  nfcd  2758  ceqsalgALT  3229  ceqsex  3239  vtocldf  3254  elrab3t  3360  morex  3388  sbciedf  3469  csbiebt  3551  csbiedf  3552  ssrd  3606  eqrd  3620  invdisj  4636  zfrepclf  4775  eusv2nf  4862  ssopab2b  5000  imadif  5971  eusvobj1  6641  ssoprab2b  6709  ovmpt2dxf  6783  axrepnd  9413  axunnd  9415  axpownd  9420  axregndlem1  9421  axacndlem1  9426  axacndlem2  9427  axacndlem3  9428  axacndlem4  9429  axacndlem5  9430  axacnd  9431  mreexexd  16302  mreexexdOLD  16303  acsmapd  17172  isch3  28082  ssrelf  29409  eqrelrd2  29410  esumeq12dvaf  30078  bnj1366  30885  bnj571  30961  bnj964  30998  iota5f  31592  bj-hbext  32685  bj-nfext  32687  bj-cbv3v2  32711  bj-abbid  32762  wl-mo3t  33338  wl-ax11-lem3  33344  cover2  33488  alrimii  33904  mpt2bi123f  33951  mptbi12f  33955  ss2iundf  37777  pm11.57  38415  pm11.59  38417  tratrb  38572  hbexg  38598  e2ebindALT  38991  mpteq1df  39265  mpteq12da  39274  dvnmul  39927  stoweidlem34  40020  sge0fodjrnlem  40402  preimagelt  40681  preimalegt  40682  pimrecltpos  40688  pimrecltneg  40702  smfaddlem1  40740  smfresal  40764  smfsupmpt  40790  smfinflem  40792  smfinfmpt  40794  ovmpt2rdxf  41888  rspcdf  42195  setrec1lem4  42208
  Copyright terms: Public domain W3C validator