Theorem alrimiv 1928

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2210 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  2071  sbimdv  2081  sbbidv  2082  elequ2g  2127  cbv3v2  2244  nexmo  2536  moimdv  2541  mobidv  2544  eubidv  2581  euequ  2592  eqrdv  2729  abbidv  2797  raleqbidvvOLD  3301  elex22  3461  pm13.183  3616  moeq3  3666  sbc2or  3745  sbcthdv  3752  csbied  3881  ssrdv  3935  eq0rdv  4354  rabeqsnd  4619  rabsn  4671  dfnfc2  4878  intab  4926  intprg  4929  iuneq12df  4966  dfiin2g  4979  abexd  5261  elALT2  5305  reusv2lem1  5334  reusv2lem2  5335  axprlem3OLD  5364  sbcop1  5426  euotd  5451  ssrelrel  5735  relimasn  6033  asymref2  6063  dfpo2  6243  iotaval2  6452  iota5  6464  iotabidv  6465  funmo  6497  funco  6521  funun  6527  fununfun  6529  fununi  6556  nfunsn  6861  fvn0ssdmfun  7007  f1oresrab  7060  0mpo0  7429  funoprabg  7467  tfisi  7789  limom  7812  funcnvuni  7862  1stconst  8030  2ndconst  8031  frxp  8056  fnwelem  8061  frxp2  8074  frxp3  8081  frrlem9  8224  seqomlem2  8370  iserd  8648  fsetdmprc0  8779  ssfi  9082  findcard3  9167  frfi  9169  fiint  9211  dffi2  9307  hartogslem1  9428  wdomd  9467  ixpiunwdom  9476  ttrclss  9610  ttrclselem2  9616  rankval3b  9719  fseqenlem2  9916  dfac3  10012  dfac5  10020  dfac2b  10022  dfac8  10027  dfac9  10028  dfacacn  10033  dfac13  10034  kmlem1  10042  kmlem6  10047  kmlem13  10054  fin23lem32  10235  axdc2lem  10339  zornn0g  10396  fpwwe2lem10  10531  fpwwe2lem11  10532  fpwwe2lem12  10533  hargch  10564  alephgch  10565  nqpr  10905  reclem2pr  10939  hashgt23el  14331  rtrclreclem4  14968  dfrtrcl2  14969  relexpindlem  14970  shftfn  14980  ramub  16925  ramcl  16941  imasaddfnlem  17432  imasvscafn  17441  mrieqv2d  17545  mreexexd  17554  invfun  17671  joinfval  18277  meetfval  18291  mreclatBAD  18469  letsr  18499  efgval  19629  efgi  19631  efgi2  19637  gsumval3lem2  19818  gsumzaddlem  19833  pgpfac1lem5  19993  ringurd  20103  zrinitorngc  20557  zrtermorngc  20558  zrtermoringc  20590  islbs3  21092  lbsextlem4  21098  cssmre  21630  obslbs  21667  mplsubglem  21936  mpllsslem  21937  tgcl  22884  indistopon  22916  ppttop  22922  epttop  22924  mretopd  23007  toponmre  23008  neissex  23042  neiptoptop  23046  lmfun  23296  2ndcdisj  23371  1stccnp  23377  kgentopon  23453  dfac14  23533  ptcnp  23537  uptx  23540  ptrescn  23554  qtoptop2  23614  filconn  23798  filssufilg  23826  rnelfmlem  23867  alexsubALTlem2  23963  cnextfun  23979  utoptop  24149  prdsxmslem2  24444  vitalilem3  25538  mbfposr  25580  mbfinf  25593  i1fd  25609  itg1climres  25642  perfdvf  25831  taylf  26295  addsbdaylem  27959  noseqrdgfn  28236  n0scut  28262  mptelee  28873  upgr1eopALT  29095  upgrspanop  29275  umgrspanop  29276  usgrspanop  29277  cplgrop  29415  umgr2v2enb1  29505  clwwlknon1loop  30078  wlkl0  30347  ex-natded9.26  30399  ex-natded9.26-2  30400  aevdemo  30440  nmcexi  32006  iuneq12daf  32536  iinabrex  32549  abfmpeld  32636  abfmpel  32637  fpwrelmap  32716  ssdifidl  33422  ssmxidl  33439  exsslsb  33609  zarclssn  33886  bnj1143  34802  bnj1379  34842  bnj149  34887  rankval4b  35111  r1omhfb  35123  r1omhfbregs  35133  fineqvac  35139  gblacfnacd  35146  vonf1owev  35152  wevgblacfn  35153  loop1cycl  35181  satffunlem1lem1  35446  satffunlem2lem1  35448  prv0  35474  mclsssvlem  35606  ssmclslem  35609  mclsax  35613  mclsind  35614  dfon2lem6  35830  dfon2lem8  35832  dfon2lem9  35833  dfon2  35834  trer  36360  finminlem  36362  neibastop1  36403  neibastop3  36406  weiunfr  36511  unbdqndv1  36552  knoppndv  36578  bj-ssbid1ALT  36709  bj-eqs  36719  bj-sb  36731  bj-substw  36766  bj-nnfbd  36770  bj-spcimdv  36939  bj-spcimdvv  36940  bj-csbprc  36954  bj-gabss  36979  bj-elgab  36983  curryset  36990  currysetlem3  36993  bj-cleq  37006  exellimddv  37389  finorwe  37426  wl-motae  37559  wl-cbvalsbi  37590  fin2so  37646  poimirlem17  37676  mblfinlem3  37698  ismblfin  37700  itg2addnc  37713  upixp  37768  mpobi123f  38201  mptbi12f  38205  preuniqval  38507  trcoss  38583  prter1  38977  axc11n-16  39036  ax12eq  39039  ax12el  39040  sticksstones22  42260  sbtd  42303  sn-axprlem3  42309  sn-exelALT  42310  ismrcd1  42790  ttac  43128  fnwe2  43145  aomclem6  43151  dfac11  43154  dfac21  43158  hbtlem2  43216  oaun3lem1  43466  cllem0  43658  clss2lem  43703  mptrcllem  43705  iunrelexpmin1  43800  iunrelexpmin2  43804  iunrelexpuztr  43811  dftrcl3  43812  brtrclfv2  43819  dfrtrcl3  43825  psshepw  43880  frege91  44046  frege97  44052  frege109  44064  frege130  44085  grumnudlem  44377  ismnushort  44393  axc11next  44498  pm13.192  44502  pm14.24  44524  gen11  44708  trsspwALT2  44910  snssiALT  44919  sstrALT2  44926  en3lpVD  44936  sspwimp  45009  sspwimpcf  45011  sspwimpALT  45016  ax6e2ndeqALT  45022  ssmapsn  45312  infnsuprnmpt  45346  uzinico  45658  icccncfext  45984  itgsinexplem1  46051  sge0resplit  46503  hoidmvlelem1  46692  hspdifhsp  46713  smflimsuplem7  46923  dfatcolem  47354  iccpartdisj  47536  sbcpr  47620  eufsnlem  48940  iscnrm3lem2  49034  functhincfun  49549  termcarweu  49628  setrec2fun  49792  elsetrecslem  49799  setrecsss  49801  setrecsres  49802  0setrec  49804  pgindnf  49816