Theorem alrimiv 1927

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2208 and 19.21v 1939. (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 1910	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	alrimih 1824	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  alrimivv  1928  cbvalivw  2007  aevlem0  2055  aev  2058  aev2  2059  stdpc4  2069  sbimdv  2079  sbbidv  2080  elequ2g  2125  cbv3v2  2242  nexmo  2534  moimdv  2539  mobidv  2542  eubidv  2579  euequ  2590  eqrdv  2727  abbidv  2795  raleqbidvvOLD  3298  elex22  3461  pm13.183  3621  moeq3  3672  sbc2or  3751  sbcthdv  3758  csbied  3887  ssrdv  3941  eq0rdv  4358  disj  4401  rabeqsnd  4621  rabsn  4673  dfnfc2  4880  intab  4928  intprg  4931  iuneq12df  4968  dfiin2g  4981  abexd  5264  elALT2  5308  reusv2lem1  5337  reusv2lem2  5338  axprlem3OLD  5367  sbcop1  5431  euotd  5456  ssrelrel  5739  asymref2  6066  dfpo2  6244  iotaval2  6453  iota5  6465  iotabidv  6466  funmo  6498  funco  6522  funun  6528  fununfun  6530  fununi  6557  nfunsn  6862  fvn0ssdmfun  7008  f1oresrab  7061  0mpo0  7432  funoprabg  7470  tfisi  7792  limom  7815  funcnvuni  7865  1stconst  8033  2ndconst  8034  frxp  8059  fnwelem  8064  frxp2  8077  frxp3  8084  frrlem9  8227  seqomlem2  8373  iserd  8651  fsetdmprc0  8782  ssfi  9087  findcard3  9172  frfi  9174  fiint  9216  fiintOLD  9217  dffi2  9313  hartogslem1  9434  wdomd  9473  ixpiunwdom  9482  ttrclss  9616  ttrclselem2  9622  rankval3b  9722  fseqenlem2  9919  dfac3  10015  dfac5  10023  dfac2b  10025  dfac8  10030  dfac9  10031  dfacacn  10036  dfac13  10037  kmlem1  10045  kmlem6  10050  kmlem13  10057  fin23lem32  10238  axdc2lem  10342  zornn0g  10399  fpwwe2lem10  10534  fpwwe2lem11  10535  fpwwe2lem12  10536  hargch  10567  alephgch  10568  nqpr  10908  reclem2pr  10942  hashgt23el  14331  cshwsexaOLD  14731  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  19596  efgi  19598  efgi2  19604  gsumval3lem2  19785  gsumzaddlem  19800  pgpfac1lem5  19960  ringurd  20070  zrinitorngc  20527  zrtermorngc  20528  zrtermoringc  20560  islbs3  21062  lbsextlem4  21068  cssmre  21600  obslbs  21637  mplsubglem  21906  mpllsslem  21907  tgcl  22854  indistopon  22886  ppttop  22892  epttop  22894  mretopd  22977  toponmre  22978  neissex  23012  neiptoptop  23016  lmfun  23266  2ndcdisj  23341  1stccnp  23347  kgentopon  23423  dfac14  23503  ptcnp  23507  uptx  23510  ptrescn  23524  qtoptop2  23584  filconn  23768  filssufilg  23796  rnelfmlem  23837  alexsubALTlem2  23933  cnextfun  23949  utoptop  24120  prdsxmslem2  24415  vitalilem3  25509  mbfposr  25551  mbfinf  25564  i1fd  25580  itg1climres  25613  perfdvf  25802  taylf  26266  addsbdaylem  27930  noseqrdgfn  28207  n0scut  28233  mptelee  28844  upgr1eopALT  29066  upgrspanop  29246  umgrspanop  29247  usgrspanop  29248  cplgrop  29386  umgr2v2enb1  29476  clwwlknon1loop  30046  wlkl0  30315  ex-natded9.26  30367  ex-natded9.26-2  30368  aevdemo  30408  nmcexi  31974  iuneq12daf  32505  iinabrex  32518  abfmpeld  32605  abfmpel  32606  fpwrelmap  32685  ssdifidl  33403  ssmxidl  33420  exsslsb  33579  zarclssn  33856  bnj1143  34773  bnj1379  34813  bnj149  34858  fineqvac  35088  gblacfnacd  35095  vonf1owev  35101  wevgblacfn  35102  loop1cycl  35130  satffunlem1lem1  35395  satffunlem2lem1  35397  prv0  35423  mclsssvlem  35555  ssmclslem  35558  mclsax  35562  mclsind  35563  dfon2lem6  35782  dfon2lem8  35784  dfon2lem9  35785  dfon2  35786  trer  36310  finminlem  36312  neibastop1  36353  neibastop3  36356  weiunfr  36461  unbdqndv1  36502  knoppndv  36528  bj-ssbid1ALT  36659  bj-eqs  36669  bj-sb  36681  bj-substw  36716  bj-nnfbd  36720  bj-spcimdv  36889  bj-spcimdvv  36890  bj-csbprc  36904  bj-gabss  36929  bj-elgab  36933  curryset  36940  currysetlem3  36943  bj-cleq  36956  exellimddv  37339  finorwe  37376  wl-motae  37509  wl-cbvalsbi  37540  fin2so  37607  poimirlem17  37637  mblfinlem3  37659  ismblfin  37661  itg2addnc  37674  upixp  37729  mpobi123f  38162  mptbi12f  38166  trcoss  38479  prter1  38878  axc11n-16  38937  ax12eq  38940  ax12el  38941  sticksstones22  42161  sbtd  42204  sn-axprlem3  42210  sn-exelALT  42211  ismrcd1  42691  ttac  43029  fnwe2  43046  aomclem6  43052  dfac11  43055  dfac21  43059  hbtlem2  43117  oaun3lem1  43367  cllem0  43559  clss2lem  43604  mptrcllem  43606  iunrelexpmin1  43701  iunrelexpmin2  43705  iunrelexpuztr  43712  dftrcl3  43713  brtrclfv2  43720  dfrtrcl3  43726  psshepw  43781  frege91  43947  frege97  43953  frege109  43965  frege130  43986  grumnudlem  44278  ismnushort  44294  axc11next  44399  pm13.192  44403  pm14.24  44425  gen11  44610  trsspwALT2  44812  snssiALT  44821  sstrALT2  44828  en3lpVD  44838  sspwimp  44911  sspwimpcf  44913  sspwimpALT  44918  ax6e2ndeqALT  44924  ssmapsn  45214  infnsuprnmpt  45248  uzinico  45560  icccncfext  45888  itgsinexplem1  45955  sge0resplit  46407  hoidmvlelem1  46596  hspdifhsp  46617  smflimsuplem7  46827  dfatcolem  47259  iccpartdisj  47441  sbcpr  47525  eufsnlem  48845  iscnrm3lem2  48939  functhincfun  49454  termcarweu  49533  setrec2fun  49697  elsetrecslem  49704  setrecsss  49706  setrecsres  49707  0setrec  49709  pgindnf  49721