Theorem alrimi 2211

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

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781

This theorem is referenced by:  sbalex  2240  sbimd  2243  sbbid  2244  nf5d  2283  axc4i  2321  19.12  2326  nfsbd  2525  mobid  2548  mo3  2562  eubid  2585  2moexv  2625  eupicka  2632  2moex  2638  2mo  2646  abbid  2808  nfcd  2896  ceqsalgALT  3516  ceqsexOLD  3529  vtocldf  3560  rspcdf  3609  elrab3t  3694  morex  3728  sbciedf  3836  csbiebt  3938  csbiedf  3939  ssrd  4000  eqrd  4015  invdisj  5134  zfrepclf  5297  eusv2nf  5401  ssopab2bw  5557  ssopab2b  5559  imadif  6652  eusvobj1  7424  ssoprab2b  7502  eqoprab2bw  7503  ovmpodxf  7583  axrepnd  10632  axunnd  10634  axpownd  10639  axregndlem1  10640  axacndlem1  10645  axacndlem2  10646  axacndlem3  10647  axacndlem4  10648  axacndlem5  10649  axacnd  10650  mreexexd  17693  acsmapd  18612  isch3  31270  ssrelf  32635  eqrelrd2  32636  esumeq12dvaf  34012  bnj1366  34822  bnj571  34899  bnj964  34936  iota5f  35704  bj-hbext  36693  bj-nfext  36695  wl-mo3t  37557  wl-ax11-lem3  37568  cover2  37702  alrimii  38106  mpobi123f  38149  mptbi12f  38153  ss2iundf  43649  pm11.57  44385  pm11.59  44387  tratrb  44534  hbexg  44554  e2ebindALT  44927  modelaxreplem2  44944  mpteq1dfOLD  45180  mpteq12daOLD  45187  dvnmul  45899  stoweidlem34  45990  sge0fodjrnlem  46372  pimrecltpos  46664  pimrecltneg  46680  smfaddlem1  46719  smfresal  46744  smfinflem  46773  ichnfim  47389  ovmpordxf  48184  setrec1lem4  48921