Theorem alrimi 2213

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785

This theorem is referenced by:  sbimd  2245  sbbid  2246  nf5d  2292  axc4i  2341  19.12  2346  cbv2OLD  2427  nfsbd  2564  mobid  2634  mo3  2648  eubid  2673  2moexv  2712  eupicka  2719  2moex  2725  2mo  2733  abbid  2887  nfcd  2968  nfabdw  3000  ceqsalgALT  3530  ceqsex  3540  vtocldf  3555  rspcdf  3610  elrab3t  3679  morex  3710  sbciedf  3813  csbiebt  3912  csbiedf  3913  ssrd  3972  eqrd  3986  invdisj  5050  zfrepclf  5198  eusv2nf  5296  ssopab2bw  5434  ssopab2b  5436  imadif  6438  eusvobj1  7150  ssoprab2b  7223  eqoprab2bw  7224  ovmpodxf  7300  axrepnd  10016  axunnd  10018  axpownd  10023  axregndlem1  10024  axacndlem1  10029  axacndlem2  10030  axacndlem3  10031  axacndlem4  10032  axacndlem5  10033  axacnd  10034  mreexexd  16919  acsmapd  17788  isch3  29018  ssrelf  30366  eqrelrd2  30367  esumeq12dvaf  31290  bnj1366  32101  bnj571  32178  bnj964  32215  iota5f  32955  bj-hbext  34044  bj-nfext  34046  wl-mo3t  34827  wl-ax11-lem3  34834  cover2  35004  alrimii  35412  mpobi123f  35455  mptbi12f  35459  ss2iundf  40024  pm11.57  40741  pm11.59  40743  tratrb  40890  hbexg  40910  e2ebindALT  41283  mpteq1df  41526  mpteq12da  41533  dvnmul  42248  stoweidlem34  42339  sge0fodjrnlem  42718  pimrecltpos  43007  pimrecltneg  43021  smfaddlem1  43059  smfresal  43083  smfsupmpt  43109  smfinflem  43111  smfinfmpt  43113  dfich2OLD  43636  ichnfim  43644  ovmpordxf  44407  setrec1lem4  44813