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  30494  ssrelf  31844  eqrelrd2  31845  esumeq12dvaf  33029  bnj1366  33840  bnj571  33917  bnj964  33954  iota5f  34693  bj-hbext  35588  bj-nfext  35590  wl-mo3t  36441  wl-ax11-lem3  36449  cover2  36583  alrimii  36987  mpobi123f  37030  mptbi12f  37034  ss2iundf  42410  pm11.57  43148  pm11.59  43150  tratrb  43297  hbexg  43317  e2ebindALT  43690  mpteq1dfOLD  43939  mpteq12daOLD  43946  dvnmul  44659  stoweidlem34  44750  sge0fodjrnlem  45132  pimrecltpos  45424  pimrecltneg  45440  smfaddlem1  45479  smfresal  45504  smfinflem  45533  smfinfmpt  45535  ichnfim  46132  ovmpordxf  47014  setrec1lem4  47735