Theorem alrimi 2204

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbimd  2235  sbbid  2236  nf5d  2278  axc4i  2313  19.12  2318  nfsbd  2519  mobid  2542  mo3  2556  eubid  2579  2moexv  2621  eupicka  2628  2moex  2634  2mo  2642  abbid  2801  nfcd  2889  nfabdwOLD  2925  ceqsalgALT  3507  ceqsexOLD  3523  vtocldf  3545  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  7406  ssoprab2b  7482  eqoprab2bw  7483  ovmpodxf  7562  axrepnd  10593  axunnd  10595  axpownd  10600  axregndlem1  10601  axacndlem1  10606  axacndlem2  10607  axacndlem3  10608  axacndlem4  10609  axacndlem5  10610  axacnd  10611  mreexexd  17598  acsmapd  18513  isch3  30759  ssrelf  32109  eqrelrd2  32110  esumeq12dvaf  33325  bnj1366  34136  bnj571  34213  bnj964  34250  iota5f  34995  bj-hbext  35893  bj-nfext  35895  wl-mo3t  36746  wl-ax11-lem3  36754  cover2  36888  alrimii  37292  mpobi123f  37335  mptbi12f  37339  ss2iundf  42714  pm11.57  43452  pm11.59  43454  tratrb  43601  hbexg  43621  e2ebindALT  43994  mpteq1dfOLD  44239  mpteq12daOLD  44246  dvnmul  44959  stoweidlem34  45050  sge0fodjrnlem  45432  pimrecltpos  45724  pimrecltneg  45740  smfaddlem1  45779  smfresal  45804  smfinflem  45833  smfinfmpt  45835  ichnfim  46432  ovmpordxf  47104  setrec1lem4  47824