Theorem alrimiv 1855

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2075 and 19.21v 1868. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
alrimiv.1	|- ( ph -> ps )

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem alrimiv

Step	Hyp	Ref	Expression
1		ax-5 1839	. 2 |- ( ph -> A. x ph )
2		alrimiv.1	. 2 |- ( ph -> ps )
3	1, 2	alrimih 1751	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem is referenced by:  alrimivv  1856  nexdvOLD  1865  nfdvOLD  1873  cbvalivw  1934  equvelv  1963  aevlem0  1980  aev  1983  hbaevg  1984  aev2ALT  1987  nf5dv  2025  euequ1  2476  axext4  2606  eqrdv  2620  abbi2dv  2742  elex2  3216  elex22  3217  spcimdv  3290  pm13.183  3344  moeq3  3383  sbc2or  3444  sbcthdv  3451  sbcimdv  3498  sbcimdvOLD  3499  ssrdv  3609  ss2abdv  3675  abssdv  3676  dfnfc2  4454  dfnfc2OLD  4455  intab  4507  iuneq12df  4544  dfiin2g  4553  disjss1  4626  mpteq12dva  4732  axsep  4780  el  4847  reusv1OLD  4867  reusv2lem1  4868  reusv2lem2  4869  reusv2lem2OLD  4870  euotd  4975  ssrelrel  5220  issref  5509  asymref2  5513  iotaval  5862  iota5  5871  iotabidv  5872  funmo  5904  funco  5928  funun  5932  fununfun  5934  fununi  5964  nfunsn  6225  fvn0ssdmfun  6350  f1oresrab  6395  funoprabg  6759  tfisi  7058  limom  7080  funcnvuni  7119  1stconst  7265  2ndconst  7266  frxp  7287  fnwelem  7292  seqomlem2  7546  iserd  7768  findcard3  8203  frfi  8205  fiint  8237  dffi2  8329  hartogslem1  8447  wdomd  8486  ixpiunwdom  8496  rankval3b  8689  fseqenlem2  8848  dfac3  8944  dfac5  8951  dfac2  8953  dfac8  8957  dfac9  8958  dfacacn  8963  dfac13  8964  kmlem1  8972  kmlem6  8977  kmlem13  8984  fin23lem32  9166  axdc2lem  9270  zornn0g  9327  brdom6disj  9354  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2lem13  9464  hargch  9495  alephgch  9496  nqpr  9836  reclem2pr  9870  cshwsexa  13570  rtrclreclem4  13801  dfrtrcl2  13802  relexpindlem  13803  shftfn  13813  ramub  15717  ramcl  15733  imasaddfnlem  16188  imasvscafn  16197  mrieqv2d  16299  mreexexd  16308  mreexexdOLD  16309  invfun  16424  joinfval  17001  meetfval  17015  mreclatBAD  17187  letsr  17227  efgval  18130  efgi  18132  efgi2  18138  gsumval3lem2  18307  gsumzaddlem  18321  pgpfac1lem5  18478  islbs3  19155  lbsextlem4  19161  mplsubglem  19434  mpllsslem  19435  cssmre  20037  obslbs  20074  tgcl  20773  indistopon  20805  ppttop  20811  epttop  20813  mretopd  20896  toponmre  20897  neissex  20931  neiptoptop  20935  lmfun  21185  2ndcdisj  21259  1stccnp  21265  kgentopon  21341  dfac14  21421  ptcnp  21425  uptx  21428  ptrescn  21442  qtoptop2  21502  filconn  21687  filssufilg  21715  rnelfmlem  21756  alexsubALTlem2  21852  cnextfun  21868  utoptop  22038  prdsxmslem2  22334  vitalilem3  23379  mbfposr  23419  mbfinf  23432  i1fd  23448  itg1climres  23481  perfdvf  23667  taylf  24115  mptelee  25775  upgr1eopALT  26012  upgrspanop  26189  umgrspanop  26190  usgrspanop  26191  cplgrop  26333  umgr2v2enb1  26422  ex-natded9.26  27276  ex-natded9.26-2  27277  aevdemo  27317  nmcexi  28885  moimd  29326  rabeqsnd  29342  iuneq12daf  29373  abfmpeld  29454  abfmpel  29455  fpwrelmap  29508  rngurd  29788  bnj145OLD  30795  bnj1143  30861  bnj1379  30901  bnj149  30945  mclsssvlem  31459  ssmclslem  31462  mclsax  31466  mclsind  31467  dfpo2  31645  dfon2lem6  31693  dfon2lem8  31695  dfon2lem9  31696  dfon2  31697  trer  32310  finminlem  32312  neibastop1  32354  neibastop3  32357  unblimceq0  32498  unbdqndv1  32499  knoppndv  32525  bj-alsb  32625  bj-ssbequ1  32644  bj-ssbid1ALT  32648  bj-eqs  32663  bj-elequ2g  32666  bj-sb  32677  bj-abbi2dv  32780  bj-axsep  32793  bj-el  32796  bj-spcimdv  32884  bj-spcimdvv  32885  bj-csbprc  32904  bj-cleq  32949  bj-ismooredr  33064  exellimddv  33193  wl-cbv3vv  33307  fin2so  33396  poimirlem17  33426  mblfinlem3  33448  ismblfin  33450  itg2addnc  33464  upixp  33524  mpt2bi123f  33971  mptbi12f  33975  prter1  34164  axc11n-16  34223  ax12eq  34226  ax12el  34227  ismrcd1  37261  ttac  37603  fnwe2  37623  aomclem6  37629  dfac11  37632  dfac21  37636  hbtlem2  37694  cllem0  37871  clss2lem  37918  mptrcllem  37920  iunrelexpmin1  38000  iunrelexpmin2  38004  iunrelexpuztr  38011  dftrcl3  38012  brtrclfv2  38019  dfrtrcl3  38025  psshepw  38082  frege91  38248  frege97  38254  frege109  38266  frege130  38287  neik0pk1imk0  38345  sbeqalbi  38601  axc11next  38607  pm13.192  38611  pm14.24  38633  sbcssOLD  38756  gen11  38841  trsspwALT2  39046  snssiALT  39063  sstrALT2  39070  en3lpVD  39080  sspwimp  39154  sspwimpcf  39156  sspwimpALT  39161  ax6e2ndeqALT  39167  rnmptpr  39358  ssmapsn  39408  infnsuprnmpt  39465  uzinico  39787  icccncfext  40100  itgsinexplem1  40169  sge0resplit  40623  hoidmvlelem1  40809  hspdifhsp  40830  smflimsuplem7  41032  funressnfv  41208  iccpartdisj  41373  zrinitorngc  42000  zrtermorngc  42001  zrtermoringc  42070  setrec2fun  42439  elsetrecslem  42444  0setrec  42447