Theorem alrimiv 1926

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem is referenced by:  alrimivv  1927  cbvalivw  2006  aevlem0  2054  aev  2057  aev2  2058  stdpc4  2068  sbimdv  2078  sbbidv  2079  elequ2g  2124  cbv3v2  2242  nexmo  2544  moimdv  2549  mobidv  2552  eubidv  2589  euequ  2600  eqrdv  2738  abbidv  2811  raleqbidvvOLD  3343  elex2OLD  3513  elex22  3514  ceqsexvOLD  3543  pm13.183  3679  moeq3  3734  sbc2or  3813  sbcthdv  3820  sbcimdvOLD  3879  csbied  3959  ssrdv  4014  abssdvOLD  4092  eq0rdv  4430  disj  4473  rabeqsnd  4691  rabsn  4746  dfnfc2  4953  intab  5002  intprg  5005  iuneq12df  5041  dfiin2g  5055  mpteq12dvaOLD  5256  abexd  5343  elALT2  5387  reusv2lem1  5416  reusv2lem2  5417  axprlem3  5443  sbcop1  5508  euotd  5532  ssrelrel  5820  asymref2  6149  dfpo2  6327  iotaval2  6541  iotavalOLD  6547  iota5  6556  iotabidv  6557  funmo  6593  funmoOLD  6594  funco  6618  funun  6624  fununfun  6626  fununi  6653  nfunsn  6962  fvn0ssdmfun  7108  f1oresrab  7161  0mpo0  7533  funoprabg  7571  tfisi  7896  limom  7919  funcnvuni  7972  1stconst  8141  2ndconst  8142  frxp  8167  fnwelem  8172  frxp2  8185  frxp3  8192  frrlem9  8335  seqomlem2  8507  iserd  8789  fsetdmprc0  8913  ssfi  9240  findcard3  9346  findcard3OLD  9347  frfi  9349  fiint  9394  fiintOLD  9395  dffi2  9492  hartogslem1  9611  wdomd  9650  ixpiunwdom  9659  ttrclss  9789  ttrclselem2  9795  rankval3b  9895  fseqenlem2  10094  dfac3  10190  dfac5  10198  dfac2b  10200  dfac8  10205  dfac9  10206  dfacacn  10211  dfac13  10212  kmlem1  10220  kmlem6  10225  kmlem13  10232  fin23lem32  10413  axdc2lem  10517  zornn0g  10574  fpwwe2lem10  10709  fpwwe2lem11  10710  fpwwe2lem12  10711  hargch  10742  alephgch  10743  nqpr  11083  reclem2pr  11117  hashgt23el  14473  cshwsexaOLD  14873  rtrclreclem4  15110  dfrtrcl2  15111  relexpindlem  15112  shftfn  15122  ramub  17060  ramcl  17076  imasaddfnlem  17588  imasvscafn  17597  mrieqv2d  17697  mreexexd  17706  invfun  17825  joinfval  18443  meetfval  18457  mreclatBAD  18633  letsr  18663  efgval  19759  efgi  19761  efgi2  19767  gsumval3lem2  19948  gsumzaddlem  19963  pgpfac1lem5  20123  ringurd  20212  zrinitorngc  20664  zrtermorngc  20665  zrtermoringc  20697  islbs3  21180  lbsextlem4  21186  cssmre  21734  obslbs  21773  mplsubglem  22042  mpllsslem  22043  tgcl  22997  indistopon  23029  ppttop  23035  epttop  23037  mretopd  23121  toponmre  23122  neissex  23156  neiptoptop  23160  lmfun  23410  2ndcdisj  23485  1stccnp  23491  kgentopon  23567  dfac14  23647  ptcnp  23651  uptx  23654  ptrescn  23668  qtoptop2  23728  filconn  23912  filssufilg  23940  rnelfmlem  23981  alexsubALTlem2  24077  cnextfun  24093  utoptop  24264  prdsxmslem2  24563  vitalilem3  25664  mbfposr  25706  mbfinf  25719  i1fd  25735  itg1climres  25769  perfdvf  25958  taylf  26420  addsbdaylem  28067  noseqrdgfn  28330  n0scut  28356  mptelee  28928  upgr1eopALT  29152  upgrspanop  29332  umgrspanop  29333  usgrspanop  29334  cplgrop  29472  umgr2v2enb1  29562  clwwlknon1loop  30130  wlkl0  30399  ex-natded9.26  30451  ex-natded9.26-2  30452  aevdemo  30492  nmcexi  32058  iuneq12daf  32579  iinabrex  32591  abfmpeld  32672  abfmpel  32673  fpwrelmap  32747  ssdifidl  33450  ssmxidl  33467  zarclssn  33819  bnj1143  34766  bnj1379  34806  bnj149  34851  fineqvac  35073  gblacfnacd  35075  wevgblacfn  35076  loop1cycl  35105  satffunlem1lem1  35370  satffunlem2lem1  35372  prv0  35398  mclsssvlem  35530  ssmclslem  35533  mclsax  35537  mclsind  35538  dfon2lem6  35752  dfon2lem8  35754  dfon2lem9  35755  dfon2  35756  trer  36282  finminlem  36284  neibastop1  36325  neibastop3  36328  weiunfr  36433  unbdqndv1  36474  knoppndv  36500  bj-ssbid1ALT  36631  bj-eqs  36641  bj-sb  36653  bj-substw  36688  bj-nnfbd  36692  bj-spcimdv  36861  bj-spcimdvv  36862  bj-csbprc  36876  bj-gabss  36901  bj-elgab  36905  curryset  36912  currysetlem3  36915  bj-cleq  36928  exellimddv  37311  finorwe  37348  wl-motae  37469  wl-cbvalsbi  37500  fin2so  37567  poimirlem17  37597  mblfinlem3  37619  ismblfin  37621  itg2addnc  37634  upixp  37689  mpobi123f  38122  mptbi12f  38126  trcoss  38438  prter1  38835  axc11n-16  38894  ax12eq  38897  ax12el  38898  sticksstones22  42125  sbtd  42204  sn-axprlem3  42210  sn-exelALT  42211  ismrcd1  42654  ttac  42993  fnwe2  43010  aomclem6  43016  dfac11  43019  dfac21  43023  hbtlem2  43081  oaun3lem1  43336  cllem0  43528  clss2lem  43573  mptrcllem  43575  iunrelexpmin1  43670  iunrelexpmin2  43674  iunrelexpuztr  43681  dftrcl3  43682  brtrclfv2  43689  dfrtrcl3  43695  psshepw  43750  frege91  43916  frege97  43922  frege109  43934  frege130  43955  grumnudlem  44254  ismnushort  44270  axc11next  44375  pm13.192  44379  pm14.24  44401  gen11  44587  trsspwALT2  44790  snssiALT  44799  sstrALT2  44806  en3lpVD  44816  sspwimp  44889  sspwimpcf  44891  sspwimpALT  44896  ax6e2ndeqALT  44902  ssmapsn  45123  infnsuprnmpt  45159  uzinico  45478  icccncfext  45808  itgsinexplem1  45875  sge0resplit  46327  hoidmvlelem1  46516  hspdifhsp  46537  smflimsuplem7  46747  dfatcolem  47170  iccpartdisj  47311  sbcpr  47395  eufsnlem  48554  iscnrm3lem2  48614  setrec2fun  48784  elsetrecslem  48791  setrecsss  48793  setrecsres  48794  0setrec  48796  pgindnf  48808