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  2568  mo3  2582  eubid  2607  2moexv  2648  eupicka  2655  2moex  2661  2mo  2669  abbid  2824  nfcd  2907  nfabdw  2940  ceqsalgALT  3446  ceqsex  3457  vtocldf  3472  rspcdf  3528  elrab3t  3601  morex  3633  sbciedf  3738  csbiebt  3834  csbiedf  3835  ssrd  3897  eqrd  3911  invdisj  5016  zfrepclf  5164  eusv2nf  5264  ssopab2bw  5404  ssopab2b  5406  imadif  6419  eusvobj1  7144  ssoprab2b  7217  eqoprab2bw  7218  ovmpodxf  7295  axrepnd  10054  axunnd  10056  axpownd  10061  axregndlem1  10062  axacndlem1  10067  axacndlem2  10068  axacndlem3  10069  axacndlem4  10070  axacndlem5  10071  axacnd  10072  mreexexd  16977  acsmapd  17854  isch3  29123  ssrelf  30477  eqrelrd2  30478  esumeq12dvaf  31518  bnj1366  32329  bnj571  32406  bnj964  32443  iota5f  33187  bj-hbext  34438  bj-nfext  34440  wl-mo3t  35257  wl-ax11-lem3  35264  cover2  35432  alrimii  35837  mpobi123f  35880  mptbi12f  35884  ss2iundf  40733  pm11.57  41466  pm11.59  41468  tratrb  41615  hbexg  41635  e2ebindALT  42008  mpteq1df  42240  mpteq12da  42247  dvnmul  42951  stoweidlem34  43042  sge0fodjrnlem  43421  pimrecltpos  43710  pimrecltneg  43724  smfaddlem1  43762  smfresal  43786  smfsupmpt  43812  smfinflem  43814  smfinfmpt  43816  ichnfim  44349  ovmpordxf  45107  setrec1lem4  45611