Theorem alrimi 2207

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎ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 1914  ax-6 1972  ax-7 2012  ax-12 2172

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

This theorem is referenced by:  sbimd  2238  sbbid  2239  nf5d  2281  axc4i  2316  19.12  2321  nfsbd  2522  mobid  2545  mo3  2559  eubid  2582  2moexv  2624  eupicka  2631  2moex  2637  2mo  2645  abbid  2804  nfcd  2892  nfabdwOLD  2928  ceqsalgALT  3509  ceqsexOLD  3525  vtocldf  3542  rspcdf  3600  elrab3t  3683  morex  3716  sbciedf  3822  csbiebt  3924  csbiedf  3925  ssrd  3988  eqrd  4002  invdisj  5133  zfrepclf  5295  eusv2nf  5394  ssopab2bw  5548  ssopab2b  5550  imadif  6633  eusvobj1  7402  ssoprab2b  7478  eqoprab2bw  7479  ovmpodxf  7558  axrepnd  10589  axunnd  10591  axpownd  10596  axregndlem1  10597  axacndlem1  10602  axacndlem2  10603  axacndlem3  10604  axacndlem4  10605  axacndlem5  10606  axacnd  10607  mreexexd  17592  acsmapd  18507  isch3  30525  ssrelf  31875  eqrelrd2  31876  esumeq12dvaf  33060  bnj1366  33871  bnj571  33948  bnj964  33985  iota5f  34724  bj-hbext  35636  bj-nfext  35638  wl-mo3t  36489  wl-ax11-lem3  36497  cover2  36631  alrimii  37035  mpobi123f  37078  mptbi12f  37082  ss2iundf  42458  pm11.57  43196  pm11.59  43198  tratrb  43345  hbexg  43365  e2ebindALT  43738  mpteq1dfOLD  43987  mpteq12daOLD  43994  dvnmul  44707  stoweidlem34  44798  sge0fodjrnlem  45180  pimrecltpos  45472  pimrecltneg  45488  smfaddlem1  45527  smfresal  45552  smfinflem  45581  smfinfmpt  45583  ichnfim  46180  ovmpordxf  47062  setrec1lem4  47783