Theorem alrimiv 1928

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

Hypothesis

Ref	Expression
alrimiv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimiv	⊢ (𝜑 → ∀𝑥𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem alrimiv

Step	Hyp	Ref	Expression
1		ax-5 1911	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	alrimih 1825	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem is referenced by:  alrimivv  1929  cbvalivw  2008  aevlem0  2057  aev  2060  aev2  2061  stdpc4  2073  sbimdv  2083  sbbidv  2084  elequ2g  2129  cbv3v2  2246  nexmo  2539  moimdv  2544  mobidv  2547  eubidv  2584  euequ  2595  eqrdv  2732  abbidv  2800  raleqbidvvOLD  3303  elex22  3463  pm13.183  3618  moeq3  3668  sbc2or  3747  sbcthdv  3754  csbied  3883  ssrdv  3937  ss2abim  4010  eq0rdv  4357  rabeqsnd  4624  rabsn  4676  dfnfc2  4883  intab  4931  intprg  4934  iuneq12df  4971  dfiin2g  4984  elALT2  5312  reusv2lem1  5341  reusv2lem2  5342  axprlem3OLD  5371  sbcop1  5434  euotd  5459  ssrelrel  5743  relimasn  6042  asymref2  6072  dfpo2  6252  iotaval2  6461  iota5  6473  iotabidv  6474  funmo  6506  funco  6530  funun  6536  fununfun  6538  fununi  6565  nfunsn  6871  fvn0ssdmfun  7017  f1oresrab  7070  0mpo0  7439  funoprabg  7477  tfisi  7799  limom  7822  funcnvuni  7872  1stconst  8040  2ndconst  8041  frxp  8066  fnwelem  8071  frxp2  8084  frxp3  8091  frrlem9  8234  seqomlem2  8380  iserd  8659  fsetdmprc0  8790  ssfi  9095  findcard3  9181  frfi  9183  fiint  9225  dffi2  9324  hartogslem1  9445  wdomd  9484  ixpiunwdom  9493  ttrclss  9627  ttrclselem2  9633  rankval3b  9736  fseqenlem2  9933  dfac3  10029  dfac5  10037  dfac2b  10039  dfac8  10044  dfac9  10045  dfacacn  10050  dfac13  10051  kmlem1  10059  kmlem6  10064  kmlem13  10071  fin23lem32  10252  zornn0g  10413  fpwwe2lem10  10549  fpwwe2lem11  10550  fpwwe2lem12  10551  hargch  10582  alephgch  10583  nqpr  10923  reclem2pr  10957  hashgt23el  14345  rtrclreclem4  14982  dfrtrcl2  14983  relexpindlem  14984  shftfn  14994  ramub  16939  ramcl  16955  imasaddfnlem  17447  imasvscafn  17456  mrieqv2d  17560  mreexexd  17569  invfun  17686  joinfval  18292  meetfval  18306  mreclatBAD  18484  letsr  18514  efgval  19644  efgi  19646  efgi2  19652  gsumval3lem2  19833  gsumzaddlem  19848  pgpfac1lem5  20008  ringurd  20118  zrinitorngc  20573  zrtermorngc  20574  zrtermoringc  20606  islbs3  21108  lbsextlem4  21114  cssmre  21646  obslbs  21683  mplsubglem  21952  mpllsslem  21953  tgcl  22911  indistopon  22943  ppttop  22949  epttop  22951  mretopd  23034  toponmre  23035  neissex  23069  neiptoptop  23073  lmfun  23323  2ndcdisj  23398  1stccnp  23404  kgentopon  23480  dfac14  23560  ptcnp  23564  uptx  23567  ptrescn  23581  qtoptop2  23641  filconn  23825  filssufilg  23853  rnelfmlem  23894  alexsubALTlem2  23990  cnextfun  24006  utoptop  24176  prdsxmslem2  24471  vitalilem3  25565  mbfposr  25607  mbfinf  25620  i1fd  25636  itg1climres  25669  perfdvf  25858  taylf  26322  addsbdaylem  27986  noseqrdgfn  28267  n0scut  28294  mpteleeOLD  28917  upgr1eopALT  29139  upgrspanop  29319  umgrspanop  29320  usgrspanop  29321  cplgrop  29459  umgr2v2enb1  29549  clwwlknon1loop  30122  wlkl0  30391  ex-natded9.26  30443  ex-natded9.26-2  30444  aevdemo  30484  nmcexi  32050  iuneq12daf  32580  iinabrex  32593  abfmpeld  32681  abfmpel  32682  ssdifidl  33487  ssmxidl  33504  exsslsb  33702  zarclssn  33979  bnj1143  34895  bnj1379  34935  bnj149  34980  rankval4b  35205  r1omhfb  35217  fineqvac  35221  r1omhfbregs  35242  gblacfnacd  35245  vonf1owev  35251  wevgblacfn  35252  loop1cycl  35280  satffunlem1lem1  35545  satffunlem2lem1  35547  prv0  35573  mclsssvlem  35705  ssmclslem  35708  mclsax  35712  mclsind  35713  dfon2lem6  35929  dfon2lem8  35931  dfon2lem9  35932  dfon2  35933  trer  36459  finminlem  36461  neibastop1  36502  neibastop3  36505  weiunfr  36610  unbdqndv1  36651  knoppndv  36677  bj-ssbid1ALT  36809  bj-eqs  36819  bj-sb  36831  bj-substw  36866  bj-nnfbd  36870  bj-spcimdv  37039  bj-spcimdvv  37040  bj-csbprc  37054  bj-gabss  37079  bj-elgab  37083  curryset  37090  currysetlem3  37093  bj-cleq  37106  exellimddv  37489  finorwe  37526  wl-motae  37659  wl-cbvalsbi  37690  fin2so  37747  poimirlem17  37777  mblfinlem3  37799  ismblfin  37801  itg2addnc  37814  upixp  37869  mpobi123f  38302  mptbi12f  38306  preuniqval  38608  trcoss  38684  prter1  39078  axc11n-16  39137  ax12eq  39140  ax12el  39141  sticksstones22  42361  sbtd  42404  sn-axprlem3  42415  sn-exelALT  42416  ismrcd1  42882  ttac  43220  fnwe2  43237  aomclem6  43243  dfac11  43246  dfac21  43250  hbtlem2  43308  oaun3lem1  43558  cllem0  43749  clss2lem  43794  mptrcllem  43796  iunrelexpmin1  43891  iunrelexpmin2  43895  iunrelexpuztr  43902  dftrcl3  43903  brtrclfv2  43910  dfrtrcl3  43916  psshepw  43971  frege91  44137  frege97  44143  frege109  44155  frege130  44176  grumnudlem  44468  ismnushort  44484  axc11next  44589  pm13.192  44593  pm14.24  44615  gen11  44799  trsspwALT2  45001  snssiALT  45010  sstrALT2  45017  en3lpVD  45027  sspwimp  45100  sspwimpcf  45102  sspwimpALT  45107  ax6e2ndeqALT  45113  ssmapsn  45402  infnsuprnmpt  45436  uzinico  45747  icccncfext  46073  itgsinexplem1  46140  sge0resplit  46592  hspdifhsp  46802  smflimsuplem7  47012  dfatcolem  47443  iccpartdisj  47625  sbcpr  47709  eufsnlem  49028  iscnrm3lem2  49122  functhincfun  49636  termcarweu  49715  setrec2fun  49879  elsetrecslem  49886  setrecsss  49888  setrecsres  49889  0setrec  49891  pgindnf  49903