Theorem alrimi 2214

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  sbalex  2243  sbimd  2246  sbbid  2247  nf5d  2285  axc4i  2323  19.12  2328  nfsbd  2527  mobid  2550  mo3  2564  eubid  2587  2moexv  2627  eupicka  2634  2moex  2640  2mo  2648  abbid  2804  nfcd  2892  ceqsalgALT  3502  ceqsexOLD  3515  vtocldf  3544  rspcdf  3593  elrab3t  3675  morex  3707  sbciedf  3813  csbiebt  3908  csbiedf  3909  ssrd  3968  eqrd  3983  invdisj  5110  zfrepclf  5266  eusv2nf  5370  ssopab2bw  5527  ssopab2b  5529  imadif  6625  eusvobj1  7403  ssoprab2b  7481  eqoprab2bw  7482  ovmpodxf  7562  axrepnd  10613  axunnd  10615  axpownd  10620  axregndlem1  10621  axacndlem1  10626  axacndlem2  10627  axacndlem3  10628  axacndlem4  10629  axacndlem5  10630  axacnd  10631  mreexexd  17665  acsmapd  18569  isch3  31227  ssrelf  32600  eqrelrd2  32601  esumeq12dvaf  34067  bnj1366  34865  bnj571  34942  bnj964  34979  iota5f  35746  bj-hbext  36733  bj-nfext  36735  wl-mo3t  37599  wl-ax11-lem3  37610  cover2  37744  alrimii  38148  mpobi123f  38191  mptbi12f  38195  ss2iundf  43658  pm11.57  44388  pm11.59  44390  tratrb  44536  hbexg  44556  e2ebindALT  44928  modelaxreplem2  44979  permaxrep  45006  dvnmul  45952  stoweidlem34  46043  sge0fodjrnlem  46425  pimrecltpos  46717  pimrecltneg  46733  smfaddlem1  46772  smfresal  46797  smfinflem  46826  ichnfim  47458  ovmpordxf  48294  setrec1lem4  49534