Theorem alrimi 2206

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786

This theorem is referenced by:  sbimd  2237  sbbid  2238  nf5d  2280  axc4i  2315  19.12  2320  nfsbd  2520  mobid  2543  mo3  2557  eubid  2580  2moexv  2622  eupicka  2629  2moex  2635  2mo  2643  abbid  2802  nfcd  2890  nfabdwOLD  2926  ceqsalgALT  3479  ceqsexOLD  3494  vtocldf  3511  rspcdf  3569  elrab3t  3647  morex  3680  sbciedf  3786  csbiebt  3888  csbiedf  3889  ssrd  3952  eqrd  3966  invdisj  5094  zfrepclf  5256  eusv2nf  5355  ssopab2bw  5509  ssopab2b  5511  imadif  6590  eusvobj1  7355  ssoprab2b  7431  eqoprab2bw  7432  ovmpodxf  7510  axrepnd  10539  axunnd  10541  axpownd  10546  axregndlem1  10547  axacndlem1  10552  axacndlem2  10553  axacndlem3  10554  axacndlem4  10555  axacndlem5  10556  axacnd  10557  mreexexd  17542  acsmapd  18457  isch3  30246  ssrelf  31601  eqrelrd2  31602  esumeq12dvaf  32719  bnj1366  33530  bnj571  33607  bnj964  33644  iota5f  34382  bj-hbext  35251  bj-nfext  35253  wl-mo3t  36104  wl-ax11-lem3  36112  cover2  36246  alrimii  36651  mpobi123f  36694  mptbi12f  36698  ss2iundf  42053  pm11.57  42791  pm11.59  42793  tratrb  42940  hbexg  42960  e2ebindALT  43333  mpteq1dfOLD  43583  mpteq12daOLD  43590  dvnmul  44304  stoweidlem34  44395  sge0fodjrnlem  44777  pimrecltpos  45069  pimrecltneg  45085  smfaddlem1  45124  smfresal  45149  smfinflem  45178  smfinfmpt  45180  ichnfim  45776  ovmpordxf  46534  setrec1lem4  47255