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

Theorem alrimi 2237
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2230. (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 2218 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1898 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1628  wnf 1855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-12 2202
This theorem depends on definitions:  df-bi 197  df-ex 1852  df-nf 1857
This theorem is referenced by:  nf5d  2280  axc4i  2294  19.12  2325  nfaldOLD  2327  cbv3v  2332  cbv3  2425  cbv2  2430  sbbid  2549  nfsbd  2591  mo3  2655  eupicka  2685  2moex  2691  2mo  2699  axbnd  2749  abbid  2888  nfcd  2907  ceqsalgALT  3380  ceqsex  3390  vtocldf  3405  elrab3t  3512  morex  3540  sbciedf  3621  csbiebt  3700  csbiedf  3701  ssrd  3755  eqrd  3769  invdisj  4770  zfrepclf  4908  eusv2nf  4992  ssopab2b  5135  imadif  6113  eusvobj1  6786  ssoprab2b  6858  ovmpt2dxf  6932  axrepnd  9617  axunnd  9619  axpownd  9624  axregndlem1  9625  axacndlem1  9630  axacndlem2  9631  axacndlem3  9632  axacndlem4  9633  axacndlem5  9634  axacnd  9635  mreexexd  16515  acsmapd  17385  isch3  28432  ssrelf  29759  eqrelrd2  29760  esumeq12dvaf  30427  bnj1366  31232  bnj571  31308  bnj964  31345  iota5f  31938  bj-hbext  33032  bj-nfext  33034  bj-abbid  33108  wl-mo3t  33685  wl-ax11-lem3  33691  cover2  33833  alrimii  34249  mpt2bi123f  34296  mptbi12f  34300  ss2iundf  38470  pm11.57  39108  pm11.59  39110  tratrb  39265  hbexg  39291  e2ebindALT  39681  mpteq1df  39955  mpteq12da  39964  dvnmul  40670  stoweidlem34  40762  sge0fodjrnlem  41144  preimagelt  41426  preimalegt  41427  pimrecltpos  41433  pimrecltneg  41447  smfaddlem1  41485  smfresal  41509  smfsupmpt  41535  smfinflem  41537  smfinfmpt  41539  ovmpt2rdxf  42635  rspcdf  42942  setrec1lem4  42955
  Copyright terms: Public domain W3C validator