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

Theorem alrimi 2207
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2201. (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 2189 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1827 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787
This theorem is referenced by:  sbimd  2238  sbbid  2239  nf5d  2281  axc4i  2316  19.12  2321  nfsbd  2525  mobid  2549  mo3  2563  eubid  2586  2moexv  2628  eupicka  2635  2moex  2641  2mo  2649  abbid  2808  nfcd  2896  nfabdwOLD  2932  ceqsalgALT  3481  ceqsexOLD  3496  vtocldf  3513  rspcdf  3571  elrab3t  3649  morex  3682  sbciedf  3788  csbiebt  3890  csbiedf  3891  ssrd  3954  eqrd  3968  invdisj  5094  zfrepclf  5256  eusv2nf  5355  ssopab2bw  5509  ssopab2b  5511  imadif  6590  eusvobj1  7355  ssoprab2b  7431  eqoprab2bw  7432  ovmpodxf  7510  axrepnd  10537  axunnd  10539  axpownd  10544  axregndlem1  10545  axacndlem1  10550  axacndlem2  10551  axacndlem3  10552  axacndlem4  10553  axacndlem5  10554  axacnd  10555  mreexexd  17535  acsmapd  18450  isch3  30225  ssrelf  31576  eqrelrd2  31577  esumeq12dvaf  32670  bnj1366  33481  bnj571  33558  bnj964  33595  iota5f  34335  bj-hbext  35204  bj-nfext  35206  wl-mo3t  36060  wl-ax11-lem3  36068  cover2  36202  alrimii  36607  mpobi123f  36650  mptbi12f  36654  ss2iundf  42005  pm11.57  42743  pm11.59  42745  tratrb  42892  hbexg  42912  e2ebindALT  43285  mpteq1dfOLD  43536  mpteq12daOLD  43543  dvnmul  44258  stoweidlem34  44349  sge0fodjrnlem  44731  pimrecltpos  45023  pimrecltneg  45039  smfaddlem1  45078  smfresal  45103  smfinflem  45132  smfinfmpt  45134  ichnfim  45730  ovmpordxf  46488  setrec1lem4  47209
  Copyright terms: Public domain W3C validator