Theorem alrimi 2255

Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2249. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
alrimi.1	⊢ Ⅎ𝑥𝜑
alrimi.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimi	⊢ (𝜑 → ∀𝑥𝜓)

Proof of Theorem alrimi

Step	Hyp	Ref	Expression
1		alrimi.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nf5ri 2237	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		alrimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	alrimih 1851	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1565  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  sbalex  2284  sbimd  2287  sbbid  2288  nf5d  2325  axc4i  2361  19.12  2366  nfsbd  2560  mobid  2584  mo3  2598  eubid  2621  2moexv  2661  eupicka  2668  2moex  2674  2mo  2682  abbid  2837  nfcd  2924  ceqsalgALT  3499  vtocldf  3535  rspcdf  3577  elrab3t  3658  morex  3691  sbciedf  3795  csbiebt  3890  csbiedf  3891  ssrd  3950  eqrd  3964  invdisj  5099  zfrepclf  5256  eusv2nf  5367  ssopab2bw  5533  ssopab2b  5535  imadif  6621  eusvobj1  7404  ssoprab2b  7480  eqoprab2bw  7481  ovmpodxf  7561  axrepnd  10579  axunnd  10581  axpownd  10586  axregndlem1  10587  axacndlem1  10592  axacndlem2  10593  axacndlem3  10594  axacndlem4  10595  axacndlem5  10596  axacnd  10597  mreexexd  17704  acsmapd  18610  isch3  31534  ssrelf  32901  eqrelrd2  32902  esumeq12dvaf  34366  bnj1366  35162  bnj571  35239  bnj964  35276  iota5f  36149  axtcond  36912  bj-nfext  37262  wl-mo3t  38153  cover2  38288  alrimii  38692  mpobi123f  38735  mptbi12f  38739  ss2iundf  44311  pm11.57  45025  pm11.59  45027  tratrb  45171  hbexg  45191  e2ebindALT  45563  modelaxreplem2  45614  permaxrep  45641  dvnmul  46583  stoweidlem34  46674  sge0fodjrnlem  47056  pimrecltpos  47348  pimrecltneg  47364  smfaddlem1  47403  smfresal  47428  smfinflem  47457  ichnfim  48136  ovmpordxf  49038  setrec1lem4  50387