Theorem alrimi 2229

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

Syntax hints:   → wi 4  ∀wal 1630  Ⅎwnf 1857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196

This theorem depends on definitions:  df-bi 197  df-ex 1854  df-nf 1859

This theorem is referenced by:  nf5d  2265  axc4i  2278  19.12  2309  nfaldOLD  2311  cbv3v  2317  cbv3  2410  cbv2  2415  sbbid  2540  nfsbd  2579  mo3  2645  eupicka  2675  2moex  2681  2mo  2689  axbnd  2739  abbid  2878  nfcd  2897  ceqsalgALT  3371  ceqsex  3381  vtocldf  3396  elrab3t  3503  morex  3531  sbciedf  3612  csbiebt  3694  csbiedf  3695  ssrd  3749  eqrd  3763  invdisj  4790  zfrepclf  4929  eusv2nf  5013  ssopab2b  5152  imadif  6134  eusvobj1  6807  ssoprab2b  6877  ovmpt2dxf  6951  axrepnd  9608  axunnd  9610  axpownd  9615  axregndlem1  9616  axacndlem1  9621  axacndlem2  9622  axacndlem3  9623  axacndlem4  9624  axacndlem5  9625  axacnd  9626  mreexexd  16510  acsmapd  17379  isch3  28407  ssrelf  29734  eqrelrd2  29735  esumeq12dvaf  30402  bnj1366  31207  bnj571  31283  bnj964  31320  iota5f  31913  bj-hbext  33007  bj-nfext  33009  bj-cbv3v2  33033  bj-abbid  33084  wl-mo3t  33671  wl-ax11-lem3  33677  cover2  33821  alrimii  34237  mpt2bi123f  34284  mptbi12f  34288  ss2iundf  38453  pm11.57  39091  pm11.59  39093  tratrb  39248  hbexg  39274  e2ebindALT  39664  mpteq1df  39942  mpteq12da  39951  dvnmul  40661  stoweidlem34  40754  sge0fodjrnlem  41136  preimagelt  41418  preimalegt  41419  pimrecltpos  41425  pimrecltneg  41439  smfaddlem1  41477  smfresal  41501  smfsupmpt  41527  smfinflem  41529  smfinfmpt  41531  ovmpt2rdxf  42627  rspcdf  42934  setrec1lem4  42947