Theorem alrimi 2211

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

Syntax hints:   → wi 4  ∀wal 1536  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  sbimd  2243  sbbid  2244  nf5d  2288  axc4i  2330  19.12  2335  cbv2OLD  2416  nfsbd  2541  mobid  2609  mo3  2623  eubid  2648  2moexv  2689  eupicka  2696  2moex  2702  2mo  2710  abbid  2864  nfcd  2944  nfabdw  2976  ceqsalgALT  3477  ceqsex  3488  vtocldf  3503  rspcdf  3558  elrab3t  3627  morex  3658  sbciedf  3761  csbiebt  3857  csbiedf  3858  ssrd  3920  eqrd  3934  invdisj  5014  zfrepclf  5162  eusv2nf  5261  ssopab2bw  5399  ssopab2b  5401  imadif  6408  eusvobj1  7129  ssoprab2b  7202  eqoprab2bw  7203  ovmpodxf  7279  axrepnd  10005  axunnd  10007  axpownd  10012  axregndlem1  10013  axacndlem1  10018  axacndlem2  10019  axacndlem3  10020  axacndlem4  10021  axacndlem5  10022  axacnd  10023  mreexexd  16911  acsmapd  17780  isch3  29024  ssrelf  30379  eqrelrd2  30380  esumeq12dvaf  31400  bnj1366  32211  bnj571  32288  bnj964  32325  iota5f  33068  bj-hbext  34157  bj-nfext  34159  wl-mo3t  34977  wl-ax11-lem3  34984  cover2  35152  alrimii  35557  mpobi123f  35600  mptbi12f  35604  ss2iundf  40360  pm11.57  41093  pm11.59  41095  tratrb  41242  hbexg  41262  e2ebindALT  41635  mpteq1df  41872  mpteq12da  41879  dvnmul  42585  stoweidlem34  42676  sge0fodjrnlem  43055  pimrecltpos  43344  pimrecltneg  43358  smfaddlem1  43396  smfresal  43420  smfsupmpt  43446  smfinflem  43448  smfinfmpt  43450  ichnfim  43981  ovmpordxf  44740  setrec1lem4  45220