Theorem alrimiv 1935

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

Syntax hints:   → wi 4  ∀wal 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem is referenced by:  alrimivv  1936  cbvalivw  2017  aevlem0  2062  aev  2065  aev2  2066  stdpc4  2076  sbimdv  2086  sbbidv  2087  elequ2g  2129  cbv3v2  2241  nexmo  2540  moimdv  2545  mobidv  2548  eubidv  2585  euequ  2596  eqrdv  2734  abbidv  2800  raleqbidvv  3305  elex2  3419  elex22  3420  ceqsexv  3445  pm13.183  3565  moeq3  3614  sbc2or  3692  sbcthdv  3699  sbcimdvOLD  3757  csbied  3836  ssrdv  3893  ss2abdvOLD  3965  abssdv  3968  eq0rdv  4305  disj  4348  rabsn  4623  dfnfc2  4829  intab  4875  intprg  4878  iuneq12df  4916  dfiin2g  4927  mpteq12dva  5124  el  5247  reusv2lem1  5276  reusv2lem2  5277  axprlem3  5303  sbcop1  5356  euotd  5381  ssrelrel  5651  asymref2  5962  iotaval  6332  iota5  6341  iotabidv  6342  funmo  6374  funco  6398  funun  6404  fununfun  6406  fununi  6433  nfunsn  6732  fvn0ssdmfun  6873  f1oresrab  6920  0mpo0  7272  funoprabg  7309  tfisi  7615  limom  7638  funcnvuni  7687  1stconst  7846  2ndconst  7847  frxp  7871  fnwelem  7876  frrlem9  8013  seqomlem2  8165  iserd  8395  fsetdmprc0  8514  ssfi  8829  findcard3  8892  frfi  8894  fiint  8926  dffi2  9017  hartogslem1  9136  wdomd  9175  ixpiunwdom  9184  rankval3b  9407  fseqenlem2  9604  dfac3  9700  dfac5  9707  dfac2b  9709  dfac8  9714  dfac9  9715  dfacacn  9720  dfac13  9721  kmlem1  9729  kmlem6  9734  kmlem13  9741  fin23lem32  9923  axdc2lem  10027  zornn0g  10084  fpwwe2lem10  10219  fpwwe2lem11  10220  fpwwe2lem12  10221  hargch  10252  alephgch  10253  nqpr  10593  reclem2pr  10627  hashgt23el  13956  cshwsexa  14354  rtrclreclem4  14589  dfrtrcl2  14590  relexpindlem  14591  shftfn  14601  ramub  16529  ramcl  16545  imasaddfnlem  16987  imasvscafn  16996  mrieqv2d  17096  mreexexd  17105  invfun  17223  joinfval  17833  meetfval  17847  mreclatBAD  18023  letsr  18053  efgval  19061  efgi  19063  efgi2  19069  gsumval3lem2  19245  gsumzaddlem  19260  pgpfac1lem5  19420  islbs3  20146  lbsextlem4  20152  cssmre  20609  obslbs  20646  mplsubglem  20915  mpllsslem  20916  tgcl  21820  indistopon  21852  ppttop  21858  epttop  21860  mretopd  21943  toponmre  21944  neissex  21978  neiptoptop  21982  lmfun  22232  2ndcdisj  22307  1stccnp  22313  kgentopon  22389  dfac14  22469  ptcnp  22473  uptx  22476  ptrescn  22490  qtoptop2  22550  filconn  22734  filssufilg  22762  rnelfmlem  22803  alexsubALTlem2  22899  cnextfun  22915  utoptop  23086  prdsxmslem2  23381  vitalilem3  24461  mbfposr  24503  mbfinf  24516  i1fd  24532  itg1climres  24566  perfdvf  24754  taylf  25207  mptelee  26940  upgr1eopALT  27162  upgrspanop  27339  umgrspanop  27340  usgrspanop  27341  cplgrop  27479  umgr2v2enb1  27568  clwwlknon1loop  28135  wlkl0  28404  ex-natded9.26  28456  ex-natded9.26-2  28457  aevdemo  28497  nmcexi  30061  rabeqsnd  30521  iuneq12daf  30569  iinabrex  30581  abfmpeld  30665  abfmpel  30666  fpwrelmap  30742  rngurd  31155  ssmxidl  31310  zarclssn  31491  bnj1143  32437  bnj1379  32477  bnj149  32522  fineqvac  32733  loop1cycl  32766  satffunlem1lem1  33031  satffunlem2lem1  33033  prv0  33059  mclsssvlem  33191  ssmclslem  33194  mclsax  33198  mclsind  33199  dfpo2  33392  dfon2lem6  33434  dfon2lem8  33436  dfon2lem9  33437  dfon2  33438  frxp2  33471  frxp3  33477  trer  34191  finminlem  34193  neibastop1  34234  neibastop3  34237  unbdqndv1  34374  knoppndv  34400  bj-ssbid1ALT  34532  bj-eqs  34542  bj-sb  34555  bj-substw  34590  bj-nnfbd  34594  bj-spcimdv  34767  bj-spcimdvv  34768  bj-csbprc  34782  bj-gabss  34809  bj-elgab  34813  curryset  34821  currysetlem3  34824  bj-cleq  34838  exellimddv  35202  finorwe  35239  wl-motae  35360  wl-cbvalsbi  35390  fin2so  35450  poimirlem17  35480  mblfinlem3  35502  ismblfin  35504  itg2addnc  35517  upixp  35573  mpobi123f  36006  mptbi12f  36010  trcoss  36286  prter1  36579  axc11n-16  36638  ax12eq  36641  ax12el  36642  sbtd  39839  sn-axprlem3  39849  sn-el  39850  ismrcd1  40164  ttac  40502  fnwe2  40522  aomclem6  40528  dfac11  40531  dfac21  40535  hbtlem2  40593  cllem0  40790  clss2lem  40836  mptrcllem  40838  iunrelexpmin1  40934  iunrelexpmin2  40938  iunrelexpuztr  40945  dftrcl3  40946  brtrclfv2  40953  dfrtrcl3  40959  psshepw  41014  frege91  41180  frege97  41186  frege109  41198  frege130  41219  grumnudlem  41517  ismnushort  41533  axc11next  41638  pm13.192  41642  pm14.24  41664  gen11  41850  trsspwALT2  42053  snssiALT  42062  sstrALT2  42069  en3lpVD  42079  sspwimp  42152  sspwimpcf  42154  sspwimpALT  42159  ax6e2ndeqALT  42165  ssmapsn  42370  infnsuprnmpt  42409  uzinico  42714  icccncfext  43046  itgsinexplem1  43113  sge0resplit  43562  hoidmvlelem1  43751  hspdifhsp  43772  smflimsuplem7  43974  dfatcolem  44362  iccpartdisj  44505  sbcpr  44589  zrinitorngc  45174  zrtermorngc  45175  zrtermoringc  45244  eufsnlem  45784  iscnrm3lem2  45844  setrec2fun  46012  elsetrecslem  46018  setrecsss  46020  setrecsres  46021  0setrec  46023