Theorem alrimi 2082

Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2075. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
alrimi.1	|- F/ x ph
alrimi.2	|- ( ph -> ps )

Assertion

Ref	Expression
alrimi	|- ( ph -> A. x ps )

Proof of Theorem alrimi

Step	Hyp	Ref	Expression
1		alrimi.1	. . 3 |- F/ x ph
2	1	nf5ri 2065	. 2 |- ( ph -> A. x ph )
3		alrimi.2	. 2 |- ( ph -> ps )
4	2, 3	alrimih 1751	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  nf5d  2118  axc4i  2131  19.12  2164  nfaldOLD  2166  cbv3v  2172  cbv3  2265  cbv2  2270  sbbid  2403  nfsbd  2442  mo3  2507  eupicka  2537  2moex  2543  2mo  2551  axbnd  2601  abbid  2740  nfcd  2759  ceqsalgALT  3231  ceqsex  3241  vtocldf  3256  elrab3t  3362  morex  3390  sbciedf  3471  csbiebt  3553  csbiedf  3554  ssrd  3608  eqrd  3622  invdisj  4638  zfrepclf  4777  eusv2nf  4864  ssopab2b  5002  imadif  5973  eusvobj1  6644  ssoprab2b  6712  ovmpt2dxf  6786  axrepnd  9416  axunnd  9418  axpownd  9423  axregndlem1  9424  axacndlem1  9429  axacndlem2  9430  axacndlem3  9431  axacndlem4  9432  axacndlem5  9433  axacnd  9434  mreexexd  16308  mreexexdOLD  16309  acsmapd  17178  isch3  28098  ssrelf  29425  eqrelrd2  29426  esumeq12dvaf  30093  bnj1366  30900  bnj571  30976  bnj964  31013  iota5f  31606  bj-hbext  32701  bj-nfext  32703  bj-cbv3v2  32727  bj-abbid  32778  wl-mo3t  33358  wl-ax11-lem3  33364  cover2  33508  alrimii  33924  mpt2bi123f  33971  mptbi12f  33975  ss2iundf  37951  pm11.57  38589  pm11.59  38591  tratrb  38746  hbexg  38772  e2ebindALT  39165  mpteq1df  39443  mpteq12da  39452  dvnmul  40158  stoweidlem34  40251  sge0fodjrnlem  40633  preimagelt  40912  preimalegt  40913  pimrecltpos  40919  pimrecltneg  40933  smfaddlem1  40971  smfresal  40995  smfsupmpt  41021  smfinflem  41023  smfinfmpt  41025  ovmpt2rdxf  42117  rspcdf  42424  setrec1lem4  42437