Theorem alrimi 2212

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783

This theorem is referenced by:  sbalex  2241  sbimd  2244  sbbid  2245  nf5d  2283  axc4i  2321  19.12  2326  nfsbd  2526  mobid  2549  mo3  2563  eubid  2586  2moexv  2626  eupicka  2633  2moex  2639  2mo  2647  abbid  2809  nfcd  2897  ceqsalgALT  3517  ceqsexOLD  3530  vtocldf  3559  rspcdf  3608  elrab3t  3690  morex  3724  sbciedf  3830  csbiebt  3927  csbiedf  3928  ssrd  3987  eqrd  4002  invdisj  5128  zfrepclf  5290  eusv2nf  5394  ssopab2bw  5551  ssopab2b  5553  imadif  6649  eusvobj1  7425  ssoprab2b  7503  eqoprab2bw  7504  ovmpodxf  7584  axrepnd  10635  axunnd  10637  axpownd  10642  axregndlem1  10643  axacndlem1  10648  axacndlem2  10649  axacndlem3  10650  axacndlem4  10651  axacndlem5  10652  axacnd  10653  mreexexd  17692  acsmapd  18600  isch3  31261  ssrelf  32628  eqrelrd2  32629  esumeq12dvaf  34033  bnj1366  34844  bnj571  34921  bnj964  34958  iota5f  35725  bj-hbext  36712  bj-nfext  36714  wl-mo3t  37578  wl-ax11-lem3  37589  cover2  37723  alrimii  38127  mpobi123f  38170  mptbi12f  38174  ss2iundf  43677  pm11.57  44413  pm11.59  44415  tratrb  44561  hbexg  44581  e2ebindALT  44954  modelaxreplem2  45001  mpteq1dfOLD  45247  mpteq12daOLD  45254  dvnmul  45963  stoweidlem34  46054  sge0fodjrnlem  46436  pimrecltpos  46728  pimrecltneg  46744  smfaddlem1  46783  smfresal  46808  smfinflem  46837  ichnfim  47456  ovmpordxf  48260  setrec1lem4  49264