Theorem alrimi 2206

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎ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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  sbimd  2237  sbbid  2238  nf5d  2281  axc4i  2316  19.12  2321  nfsbd  2526  mobid  2550  mo3  2564  eubid  2587  2moexv  2629  eupicka  2636  2moex  2642  2mo  2650  abbid  2809  nfcd  2895  nfabdwOLD  2931  ceqsalgALT  3465  ceqsex  3478  vtocldf  3493  rspcdf  3548  elrab3t  3623  morex  3654  sbciedf  3760  csbiebt  3862  csbiedf  3863  ssrd  3926  eqrd  3940  invdisj  5058  zfrepclf  5218  eusv2nf  5318  ssopab2bw  5460  ssopab2b  5462  imadif  6518  eusvobj1  7269  ssoprab2b  7344  eqoprab2bw  7345  ovmpodxf  7423  axrepnd  10350  axunnd  10352  axpownd  10357  axregndlem1  10358  axacndlem1  10363  axacndlem2  10364  axacndlem3  10365  axacndlem4  10366  axacndlem5  10367  axacnd  10368  mreexexd  17357  acsmapd  18272  isch3  29603  ssrelf  30955  eqrelrd2  30956  esumeq12dvaf  31999  bnj1366  32809  bnj571  32886  bnj964  32923  iota5f  33669  bj-hbext  34892  bj-nfext  34894  wl-mo3t  35731  wl-ax11-lem3  35738  cover2  35872  alrimii  36277  mpobi123f  36320  mptbi12f  36324  ss2iundf  41267  pm11.57  42007  pm11.59  42009  tratrb  42156  hbexg  42176  e2ebindALT  42549  mpteq1dfOLD  42780  mpteq12daOLD  42787  dvnmul  43484  stoweidlem34  43575  sge0fodjrnlem  43954  pimrecltpos  44245  pimrecltneg  44260  smfaddlem1  44298  smfresal  44322  smfinflem  44350  smfinfmpt  44352  ichnfim  44916  ovmpordxf  45674  setrec1lem4  46396