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  27928  noseqrdgfn  28205  n0scut  28231  mptelee  28840  upgr1eopALT  29062  upgrspanop  29242  umgrspanop  29243  usgrspanop  29244  cplgrop  29382  umgr2v2enb1  29472  clwwlknon1loop  30042  wlkl0  30311  ex-natded9.26  30363  ex-natded9.26-2  30364  aevdemo  30404  nmcexi  31970  iuneq12daf  32500  iinabrex  32513  abfmpeld  32598  abfmpel  32599  fpwrelmap  32677  ssdifidl  33395  ssmxidl  33412  exsslsb  33569  zarclssn  33846  bnj1143  34763  bnj1379  34803  bnj149  34848  fineqvac  35078  gblacfnacd  35085  vonf1owev  35091  wevgblacfn  35092  loop1cycl  35120  satffunlem1lem1  35385  satffunlem2lem1  35387  prv0  35413  mclsssvlem  35545  ssmclslem  35548  mclsax  35552  mclsind  35553  dfon2lem6  35772  dfon2lem8  35774  dfon2lem9  35775  dfon2  35776  trer  36300  finminlem  36302  neibastop1  36343  neibastop3  36346  weiunfr  36451  unbdqndv1  36492  knoppndv  36518  bj-ssbid1ALT  36649  bj-eqs  36659  bj-sb  36671  bj-substw  36706  bj-nnfbd  36710  bj-spcimdv  36879  bj-spcimdvv  36880  bj-csbprc  36894  bj-gabss  36919  bj-elgab  36923  curryset  36930  currysetlem3  36933  bj-cleq  36946  exellimddv  37329  finorwe  37366  wl-motae  37499  wl-cbvalsbi  37530  fin2so  37597  poimirlem17  37627  mblfinlem3  37649  ismblfin  37651  itg2addnc  37664  upixp  37719  mpobi123f  38152  mptbi12f  38156  trcoss  38469  prter1  38868  axc11n-16  38927  ax12eq  38930  ax12el  38931  sticksstones22  42151  sbtd  42194  sn-axprlem3  42200  sn-exelALT  42201  ismrcd1  42681  ttac  43019  fnwe2  43036  aomclem6  43042  dfac11  43045  dfac21  43049  hbtlem2  43107  oaun3lem1  43357  cllem0  43549  clss2lem  43594  mptrcllem  43596  iunrelexpmin1  43691  iunrelexpmin2  43695  iunrelexpuztr  43702  dftrcl3  43703  brtrclfv2  43710  dfrtrcl3  43716  psshepw  43771  frege91  43937  frege97  43943  frege109  43955  frege130  43976  grumnudlem  44268  ismnushort  44284  axc11next  44389  pm13.192  44393  pm14.24  44415  gen11  44600  trsspwALT2  44802  snssiALT  44811  sstrALT2  44818  en3lpVD  44828  sspwimp  44901  sspwimpcf  44903  sspwimpALT  44908  ax6e2ndeqALT  44914  ssmapsn  45204  infnsuprnmpt  45238  uzinico  45550  icccncfext  45878  itgsinexplem1  45945  sge0resplit  46397  hoidmvlelem1  46586  hspdifhsp  46607  smflimsuplem7  46817  dfatcolem  47249  iccpartdisj  47431  sbcpr  47515  eufsnlem  48835  iscnrm3lem2  48929  functhincfun  49444  termcarweu  49523  setrec2fun  49687  elsetrecslem  49694  setrecsss  49696  setrecsres  49697  0setrec  49699  pgindnf  49711