Theorem alrimi 2209

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

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

This theorem is referenced by:  sbimd  2240  sbbid  2241  nf5d  2284  axc4i  2320  19.12  2325  nfsbd  2526  mobid  2550  mo3  2564  eubid  2587  2moexv  2629  eupicka  2636  2moex  2642  2mo  2650  abbid  2810  nfcd  2894  nfabdwOLD  2930  ceqsalgALT  3455  ceqsex  3468  vtocldf  3483  rspcdf  3538  elrab3t  3616  morex  3649  sbciedf  3755  csbiebt  3858  csbiedf  3859  ssrd  3922  eqrd  3936  invdisj  5054  zfrepclf  5213  eusv2nf  5313  ssopab2bw  5453  ssopab2b  5455  imadif  6502  eusvobj1  7249  ssoprab2b  7322  eqoprab2bw  7323  ovmpodxf  7401  axrepnd  10281  axunnd  10283  axpownd  10288  axregndlem1  10289  axacndlem1  10294  axacndlem2  10295  axacndlem3  10296  axacndlem4  10297  axacndlem5  10298  axacnd  10299  mreexexd  17274  acsmapd  18187  isch3  29504  ssrelf  30856  eqrelrd2  30857  esumeq12dvaf  31899  bnj1366  32709  bnj571  32786  bnj964  32823  iota5f  33571  bj-hbext  34819  bj-nfext  34821  wl-mo3t  35658  wl-ax11-lem3  35665  cover2  35799  alrimii  36204  mpobi123f  36247  mptbi12f  36251  ss2iundf  41156  pm11.57  41896  pm11.59  41898  tratrb  42045  hbexg  42065  e2ebindALT  42438  mpteq1dfOLD  42669  mpteq12daOLD  42676  dvnmul  43374  stoweidlem34  43465  sge0fodjrnlem  43844  pimrecltpos  44133  pimrecltneg  44147  smfaddlem1  44185  smfresal  44209  smfinflem  44237  smfinfmpt  44239  ichnfim  44804  ovmpordxf  45562  setrec1lem4  46282