Theorem alrimi 2198

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

Syntax hints:   → wi 4  ∀wal 1531  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2163

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  sbimd  2229  sbbid  2230  nf5d  2272  axc4i  2307  19.12  2312  nfsbd  2513  mobid  2536  mo3  2550  eubid  2573  2moexv  2615  eupicka  2622  2moex  2628  2mo  2636  abbid  2795  nfcd  2883  nfabdwOLD  2919  ceqsalgALT  3501  ceqsexOLD  3517  vtocldf  3539  rspcdf  3591  elrab3t  3675  morex  3708  sbciedf  3814  csbiebt  3916  csbiedf  3917  ssrd  3980  eqrd  3994  invdisj  5123  zfrepclf  5285  eusv2nf  5384  ssopab2bw  5538  ssopab2b  5540  imadif  6623  eusvobj1  7395  ssoprab2b  7471  eqoprab2bw  7472  ovmpodxf  7551  axrepnd  10586  axunnd  10588  axpownd  10593  axregndlem1  10594  axacndlem1  10599  axacndlem2  10600  axacndlem3  10601  axacndlem4  10602  axacndlem5  10603  axacnd  10604  mreexexd  17593  acsmapd  18511  isch3  30966  ssrelf  32316  eqrelrd2  32317  esumeq12dvaf  33521  bnj1366  34331  bnj571  34408  bnj964  34445  iota5f  35190  bj-hbext  36079  bj-nfext  36081  wl-mo3t  36935  wl-ax11-lem3  36943  cover2  37077  alrimii  37481  mpobi123f  37524  mptbi12f  37528  ss2iundf  42924  pm11.57  43662  pm11.59  43664  tratrb  43811  hbexg  43831  e2ebindALT  44204  mpteq1dfOLD  44449  mpteq12daOLD  44456  dvnmul  45169  stoweidlem34  45260  sge0fodjrnlem  45642  pimrecltpos  45934  pimrecltneg  45950  smfaddlem1  45989  smfresal  46014  smfinflem  46043  smfinfmpt  46045  ichnfim  46642  ovmpordxf  47228  setrec1lem4  47947