Theorem alrimi 2249

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

Syntax hints:   → wi 4  ∀wal 1559  Ⅎwnf 1804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-12 2213

This theorem depends on definitions:  df-bi 209  df-ex 1801  df-nf 1805

This theorem is referenced by:  sbalex  2278  sbimd  2281  sbbid  2282  nf5d  2319  axc4i  2355  19.12  2360  nfsbd  2554  mobid  2578  mo3  2592  eubid  2615  2moexv  2655  eupicka  2662  2moex  2668  2mo  2676  abbid  2831  nfcd  2918  ceqsalgALT  3491  vtocldf  3527  rspcdf  3569  elrab3t  3650  morex  3683  sbciedf  3787  csbiebt  3882  csbiedf  3883  ssrd  3942  eqrd  3956  invdisj  5087  zfrepclf  5242  eusv2nf  5353  ssopab2bw  5519  ssopab2b  5521  imadif  6606  eusvobj1  7390  ssoprab2b  7466  eqoprab2bw  7467  ovmpodxf  7547  axrepnd  10553  axunnd  10555  axpownd  10560  axregndlem1  10561  axacndlem1  10566  axacndlem2  10567  axacndlem3  10568  axacndlem4  10569  axacndlem5  10570  axacnd  10571  mreexexd  17681  acsmapd  18587  isch3  31445  ssrelf  32818  eqrelrd2  32819  esumeq12dvaf  34329  bnj1366  35125  bnj571  35202  bnj964  35239  iota5f  36075  axtcond  36839  bj-nfext  37190  wl-mo3t  38080  cover2  38215  alrimii  38619  mpobi123f  38662  mptbi12f  38666  ss2iundf  44236  pm11.57  44966  pm11.59  44968  tratrb  45113  hbexg  45133  e2ebindALT  45505  modelaxreplem2  45556  permaxrep  45583  dvnmul  46518  stoweidlem34  46609  sge0fodjrnlem  46991  pimrecltpos  47283  pimrecltneg  47299  smfaddlem1  47338  smfresal  47363  smfinflem  47392  ichnfim  48071  ovmpordxf  48962  setrec1lem4  50312