Theorem alrimi 2225

Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2219. (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 2207	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3		alrimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	alrimih 1831	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1545  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  sbalex  2254  sbimd  2257  sbbid  2258  nf5d  2295  axc4i  2331  19.12  2336  nfsbd  2530  mobid  2554  mo3  2568  eubid  2591  2moexv  2631  eupicka  2638  2moex  2644  2mo  2652  abbid  2807  nfcd  2894  ceqsalgALT  3467  vtocldf  3505  rspcdf  3547  elrab3t  3628  morex  3660  sbciedf  3765  csbiebt  3860  csbiedf  3861  ssrd  3920  eqrd  3934  invdisj  5058  zfrepclf  5213  eusv2nf  5324  ssopab2bw  5489  ssopab2b  5491  imadif  6569  eusvobj1  7349  ssoprab2b  7425  eqoprab2bw  7426  ovmpodxf  7506  axrepnd  10508  axunnd  10510  axpownd  10515  axregndlem1  10516  axacndlem1  10521  axacndlem2  10522  axacndlem3  10523  axacndlem4  10524  axacndlem5  10525  axacnd  10526  mreexexd  17605  acsmapd  18511  isch3  31330  ssrelf  32707  eqrelrd2  32708  esumeq12dvaf  34215  bnj1366  35011  bnj571  35088  bnj964  35125  iota5f  35952  axtcond  36706  bj-nfext  37057  wl-mo3t  37947  cover2  38082  alrimii  38486  mpobi123f  38529  mptbi12f  38533  ss2iundf  44103  pm11.57  44833  pm11.59  44835  tratrb  44980  hbexg  45000  e2ebindALT  45372  modelaxreplem2  45423  permaxrep  45450  dvnmul  46386  stoweidlem34  46477  sge0fodjrnlem  46859  pimrecltpos  47151  pimrecltneg  47167  smfaddlem1  47206  smfresal  47231  smfinflem  47260  ichnfim  47939  ovmpordxf  48830  setrec1lem4  50180