Theorem alrimi 2214

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbalex  2243  sbimd  2246  sbbid  2247  nf5d  2284  axc4i  2321  19.12  2326  nfsbd  2520  mobid  2543  mo3  2557  eubid  2580  2moexv  2620  eupicka  2627  2moex  2633  2mo  2641  abbid  2797  nfcd  2884  ceqsalgALT  3473  ceqsexOLD  3486  vtocldf  3515  rspcdf  3564  elrab3t  3647  morex  3679  sbciedf  3785  csbiebt  3880  csbiedf  3881  ssrd  3940  eqrd  3955  invdisj  5078  zfrepclf  5230  eusv2nf  5334  ssopab2bw  5490  ssopab2b  5492  imadif  6566  eusvobj1  7342  ssoprab2b  7418  eqoprab2bw  7419  ovmpodxf  7499  axrepnd  10488  axunnd  10490  axpownd  10495  axregndlem1  10496  axacndlem1  10501  axacndlem2  10502  axacndlem3  10503  axacndlem4  10504  axacndlem5  10505  axacnd  10506  mreexexd  17554  acsmapd  18460  isch3  31185  ssrelf  32560  eqrelrd2  32561  esumeq12dvaf  34004  bnj1366  34802  bnj571  34879  bnj964  34916  iota5f  35707  bj-hbext  36694  bj-nfext  36696  wl-mo3t  37560  wl-ax11-lem3  37571  cover2  37705  alrimii  38109  mpobi123f  38152  mptbi12f  38156  ss2iundf  43642  pm11.57  44372  pm11.59  44374  tratrb  44520  hbexg  44540  e2ebindALT  44912  modelaxreplem2  44963  permaxrep  44990  dvnmul  45934  stoweidlem34  46025  sge0fodjrnlem  46407  pimrecltpos  46699  pimrecltneg  46715  smfaddlem1  46754  smfresal  46779  smfinflem  46808  ichnfim  47458  ovmpordxf  48333  setrec1lem4  49685