Theorem alrimi 2080

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

Syntax hints:   → wi 4  ∀wal 1478  Ⅎwnf 1705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707

This theorem is referenced by:  nf5d  2115  axc4i  2127  19.12  2161  nfaldOLD  2163  cbv3v  2169  cbv3  2264  cbv2  2269  cbvalv  2272  sbbid  2402  nfsbd  2441  mo3  2506  eupicka  2536  2moex  2542  2mo  2550  axbnd  2600  abbid  2737  nfcd  2756  ceqsalgALT  3217  ceqsex  3227  vtocldf  3242  elrab3t  3345  morex  3372  sbciedf  3453  csbiebt  3534  csbiedf  3535  ssrd  3588  invdisj  4601  zfrepclf  4737  eusv2nf  4824  ssopab2b  4962  imadif  5931  eusvobj1  6598  ssoprab2b  6665  ovmpt2dxf  6739  axrepnd  9360  axunnd  9362  axpownd  9367  axregndlem1  9368  axacndlem1  9373  axacndlem2  9374  axacndlem3  9375  axacndlem4  9376  axacndlem5  9377  axacnd  9378  mreexexd  16229  mreexexdOLD  16230  acsmapd  17099  isch3  27947  ssrelf  29268  eqrelrd2  29269  esumeq12dvaf  29874  bnj1366  30608  bnj571  30684  bnj964  30721  iota5f  31315  bj-hbext  32343  bj-nfext  32345  bj-cbv3v2  32369  bj-abbid  32421  wl-mo3t  32990  wl-ax11-lem3  32996  cover2  33140  alrimii  33556  mpt2bi123f  33603  mptbi12f  33607  ss2iundf  37432  pm11.57  38071  pm11.59  38073  tratrb  38228  hbexg  38254  e2ebindALT  38648  mpteq1df  38918  mpteq12da  38927  dvnmul  39464  stoweidlem34  39558  sge0fodjrnlem  39940  preimagelt  40219  preimalegt  40220  pimrecltpos  40226  pimrecltneg  40240  smfaddlem1  40278  smfresal  40302  smfsupmpt  40328  smfinflem  40330  smfinfmpt  40332  ovmpt2rdxf  41405  rspcdf  41716  setrec1lem4  41730