Theorem alrimi 2069

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

Syntax hints:   → wi 4  ∀wal 1473  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701

This theorem is referenced by:  nf5d  2104  axc4i  2116  19.12  2150  nfaldOLD  2152  cbv3v  2158  cbv3  2253  cbv2  2258  cbvalv  2261  sbbid  2391  nfsbd  2430  mo3  2495  eupicka  2525  2moex  2531  2mo  2539  axbnd  2589  abbid  2727  nfcd  2746  ceqsalgALT  3204  ceqsex  3214  vtocldf  3229  elrab3t  3330  morex  3357  sbciedf  3438  csbiebt  3519  csbiedf  3520  ssrd  3573  invdisj  4571  zfrepclf  4705  eusv2nf  4790  ssopab2b  4927  imadif  5887  eusvobj1  6543  ssoprab2b  6610  ovmpt2dxf  6684  axrepnd  9295  axunnd  9297  axpownd  9302  axregndlem1  9303  axacndlem1  9308  axacndlem2  9309  axacndlem3  9310  axacndlem4  9311  axacndlem5  9312  axacnd  9313  mreexexd  16131  mreexexdOLD  16132  acsmapd  17001  isch3  27482  ssrelf  28805  eqrelrd2  28806  esumeq12dvaf  29420  bnj1366  30154  bnj571  30230  bnj964  30267  iota5f  30861  bj-hbext  31888  bj-nfext  31890  bj-cbv3v2  31914  bj-abbid  31966  wl-mo3t  32537  wl-ax11-lem3  32543  cover2  32678  alrimii  33094  mpt2bi123f  33141  mptbi12f  33145  ss2iundf  36970  pm11.57  37611  pm11.59  37613  tratrb  37767  hbexg  37793  e2ebindALT  38187  dvnmul  38833  stoweidlem34  38927  sge0fodjrnlem  39309  preimagelt  39589  preimalegt  39590  pimrecltpos  39596  pimrecltneg  39610  smfaddlem1  39649  smfresal  39673  ovmpt2rdxf  41910  rspcdf  42222  setrec1lem4  42236