Theorem alrimiv 1905

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

Syntax hints:   → wi 4  ∀wal 1520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1777  ax-4 1791  ax-5 1888

This theorem is referenced by:  alrimivv  1906  cbvalivw  1991  aevlem0  2030  aev  2033  hbaevg  2034  aev2ALT  2040  stdpc4  2046  sbimdv  2056  sbbidv  2057  elequ2g  2098  cbv3v2  2208  nexmo  2577  moimdv  2583  mobidv  2588  eubidv  2632  euequ  2642  euequOLD  2643  eqrdv  2793  abbidv  2860  abbi2dvOLD  2920  elex2  3459  elex22  3460  spcimdv  3535  pm13.183  3598  pm13.183OLD  3599  moeq3  3642  sbc2or  3718  sbcthdv  3725  sbcimdv  3775  ssrdv  3899  ss2abdv  3969  abssdv  3970  rabsn  4568  dfnfc2  4767  intab  4816  iuneq12df  4854  dfiin2g  4864  mpteq12dva  5049  el  5166  reusv2lem1  5195  reusv2lem2  5196  axprlem3  5222  sbcop1  5276  euotd  5299  ssrelrel  5560  asymref2  5858  iotaval  6205  iota5  6214  iotabidv  6215  funmo  6246  funco  6270  funun  6275  fununfun  6277  fununi  6304  nfunsn  6580  fvn0ssdmfun  6712  f1oresrab  6757  funoprabg  7134  tfisi  7434  limom  7456  funcnvuni  7497  1stconst  7656  2ndconst  7657  frxp  7678  fnwelem  7683  seqomlem2  7943  iserd  8170  findcard3  8612  frfi  8614  fiint  8646  dffi2  8738  hartogslem1  8857  wdomd  8896  ixpiunwdom  8906  rankval3b  9106  fseqenlem2  9302  dfac3  9398  dfac5  9405  dfac2b  9407  dfac8  9412  dfac9  9413  dfacacn  9418  dfac13  9419  kmlem1  9427  kmlem6  9432  kmlem13  9439  fin23lem32  9617  axdc2lem  9721  zornn0g  9778  fpwwe2lem11  9913  fpwwe2lem12  9914  fpwwe2lem13  9915  hargch  9946  alephgch  9947  nqpr  10287  reclem2pr  10321  hashgt23el  13638  cshwsexa  14027  rtrclreclem4  14259  dfrtrcl2  14260  relexpindlem  14261  shftfn  14271  ramub  16183  ramcl  16199  imasaddfnlem  16635  imasvscafn  16644  mrieqv2d  16744  mreexexd  16753  invfun  16868  joinfval  17445  meetfval  17459  mreclatBAD  17631  letsr  17671  efgval  18575  efgi  18577  efgi2  18583  gsumval3lem2  18752  gsumzaddlem  18766  pgpfac1lem5  18923  islbs3  19622  lbsextlem4  19628  mplsubglem  19907  mpllsslem  19908  cssmre  20524  obslbs  20561  tgcl  21266  indistopon  21298  ppttop  21304  epttop  21306  mretopd  21389  toponmre  21390  neissex  21424  neiptoptop  21428  lmfun  21678  2ndcdisj  21753  1stccnp  21759  kgentopon  21835  dfac14  21915  ptcnp  21919  uptx  21922  ptrescn  21936  qtoptop2  21996  filconn  22180  filssufilg  22208  rnelfmlem  22249  alexsubALTlem2  22345  cnextfun  22361  utoptop  22531  prdsxmslem2  22827  vitalilem3  23899  mbfposr  23941  mbfinf  23954  i1fd  23970  itg1climres  24003  perfdvf  24189  taylf  24637  mptelee  26369  upgr1eopALT  26590  upgrspanop  26767  umgrspanop  26768  usgrspanop  26769  cplgrop  26907  umgr2v2enb1  26996  clwwlknon1loop  27569  wlkl0  27843  ex-natded9.26  27895  ex-natded9.26-2  27896  aevdemo  27936  nmcexi  29499  rabeqsnd  29961  iuneq12daf  30003  abfmpeld  30094  abfmpel  30095  fpwrelmap  30162  rngurd  30516  bnj1143  31684  bnj1379  31724  bnj149  31768  loop1cycl  31998  satffunlem1lem1  32263  satffunlem2lem1  32265  prv0  32291  mclsssvlem  32423  ssmclslem  32426  mclsax  32430  mclsind  32431  dfpo2  32605  dfon2lem6  32647  dfon2lem8  32649  dfon2lem9  32650  dfon2  32651  frrlem9  32746  trer  33279  finminlem  33281  neibastop1  33322  neibastop3  33325  unbdqndv1  33462  knoppndv  33488  bj-ssbid1ALT  33606  bj-eqs  33616  bj-sb  33629  bj-abbi2dv  33706  bj-el  33713  bj-spcimdv  33793  bj-spcimdvv  33794  bj-csbprc  33807  curryset  33838  currysetlem3  33841  bj-cleq  33855  bj-nnfbd  33859  exellimddv  34182  finorwe  34219  wl-motae  34311  fin2so  34435  poimirlem17  34465  mblfinlem3  34487  ismblfin  34489  itg2addnc  34502  upixp  34561  mpobi123f  34997  mptbi12f  35001  trcoss  35278  prter1  35571  axc11n-16  35630  ax12eq  35633  ax12el  35634  sn-axprlem3  38664  sn-el  38665  ismrcd1  38805  ttac  39143  fnwe2  39163  aomclem6  39169  dfac11  39172  dfac21  39176  hbtlem2  39234  cllem0  39435  clss2lem  39481  mptrcllem  39483  iunrelexpmin1  39563  iunrelexpmin2  39567  iunrelexpuztr  39574  dftrcl3  39575  brtrclfv2  39582  dfrtrcl3  39588  psshepw  39644  frege91  39810  frege97  39816  frege109  39828  frege130  39849  grumnudlem  40143  axc11next  40301  pm13.192  40305  pm14.24  40327  gen11  40514  trsspwALT2  40717  snssiALT  40726  sstrALT2  40733  en3lpVD  40743  sspwimp  40816  sspwimpcf  40818  sspwimpALT  40823  ax6e2ndeqALT  40829  ssmapsn  41044  infnsuprnmpt  41088  uzinico  41403  icccncfext  41737  itgsinexplem1  41806  sge0resplit  42256  hoidmvlelem1  42445  hspdifhsp  42466  smflimsuplem7  42668  dfatcolem  42996  iccpartdisj  43105  sbcpr  43191  zrinitorngc  43775  zrtermorngc  43776  zrtermoringc  43845  setrec2fun  44301  elsetrecslem  44307  setrecsss  44309  setrecsres  44310  0setrec  44312