Theorem alrimiv 1949

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

Syntax hints:   → wi 4  ∀wal 1560

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

This theorem is referenced by:  alrimivv  1950  cbvalivw  2029  aevlem0  2078  aev  2081  aev2  2082  stdpc4lem  2099  stdpc4ALT  2101  sbimdv  2113  sbbidv  2114  elequ2g  2160  cbv3v2  2278  nexmo  2570  moimdv  2575  mobidv  2578  eubidv  2615  euequ  2626  eqrdv  2762  abbidv  2830  elex22  3480  pm13.183  3627  moeq3  3677  sbc2or  3755  sbcthdv  3762  csbied  3890  ssrdv  3944  eq0rdv  4363  rabeqsnd  4630  rabsn  4682  dfnfc2  4889  intab  4938  iuneq12df  4978  elALT2  5328  reusv2lem1  5357  reusv2lem2  5358  axprlem3OLD  5388  sbcop1  5458  euotd  5484  ssrelrel  5770  relimasn  6076  asymref2  6106  dfpo2  6285  iotaval2  6494  iota5  6506  iotabidv  6507  funmo  6539  funco  6563  funun  6569  fununfun  6571  fununi  6598  nfunsn  6908  fvn0ssdmfun  7057  f1oresrab  7111  0mpo0  7481  funoprabg  7519  tfisi  7841  limom  7864  funcnvuni  7915  1stconst  8081  2ndconst  8082  frxp  8108  fnwelem  8113  frxp2  8126  frxp3  8133  frrlem9  8277  seqomlem2  8424  iserd  8707  fsetdmprc0  8838  ssfi  9143  findcard3  9229  frfi  9231  fiint  9273  dffi2  9371  hartogslem1  9492  wdomd  9531  ixpiunwdom  9540  ttrclss  9677  ttrclselem2  9683  rankval3b  9786  fseqenlem2  9983  dfac3  10079  dfac5  10087  dfac2b  10089  dfac8  10094  dfac9  10095  dfacacn  10100  dfac13  10101  kmlem1  10109  kmlem6  10114  kmlem13  10121  fin23lem32  10303  zornn0g  10464  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2lem12  10602  hargch  10633  alephgch  10634  nqpr  10974  reclem2pr  11008  hashgt23el  14439  rtrclreclem4  15076  dfrtrcl2  15077  relexpindlem  15078  shftfn  15088  ramub  17051  ramcl  17067  imasaddfnlem  17560  imasvscafn  17569  mrieqv2d  17673  mreexexd  17682  invfun  17799  joinfval  18405  meetfval  18419  mreclatBAD  18597  letsr  18627  efgval  19759  efgi  19761  efgi2  19767  gsumval3lem2  19948  gsumzaddlem  19963  pgpfac1lem5  20123  ringurd  20237  zrinitorngc  20694  zrtermorngc  20695  zrtermoringc  20727  islbs3  21227  lbsextlem4  21233  cssmre  21747  obslbs  21784  mplsubglem  22052  mpllsslem  22053  tgcl  23031  indistopon  23063  ppttop  23069  epttop  23071  mretopd  23154  toponmre  23155  neissex  23189  neiptoptop  23193  lmfun  23443  2ndcdisj  23518  1stccnp  23524  kgentopon  23600  dfac14  23680  ptcnp  23684  uptx  23687  ptrescn  23701  qtoptop2  23761  filconn  23945  filssufilg  23973  rnelfmlem  24014  alexsubALTlem2  24110  cnextfun  24126  utoptop  24296  prdsxmslem2  24591  vitalilem3  25674  mbfposr  25716  mbfinf  25729  i1fd  25745  itg1climres  25778  perfdvf  25967  taylf  26426  addbdaylem  28112  noseqrdgfn  28401  n0cut  28429  mpteleeOLD  29098  upgr1eopALT  29320  upgrspanop  29500  umgrspanop  29501  usgrspanop  29502  cplgrop  29640  umgr2v2enb1  29729  clwwlknon1loop  30302  wlkl0  30571  ex-natded9.26  30623  ex-natded9.26-2  30624  aevdemo  30664  nmcexi  32231  iuneq12daf  32758  iinabrex  32771  abfmpeld  32858  abfmpel  32859  ssdifidl  33646  ssmxidl  33664  exsslsb  33896  zarclssn  34172  bnj1143  35087  bnj1379  35127  bnj149  35172  rankval4b  35400  r1omhfb  35412  fineqvac  35416  r1omhfbregs  35437  gblacfnacd  35449  vonf1wev  35455  vonf1owevOLD  35457  wevgblacfn  35458  loop1cycl  35492  satffunlem1lem1  35757  satffunlem2lem1  35759  prv0  35785  mclsssvlem  35917  ssmclslem  35920  mclsax  35924  mclsind  35925  dfon2lem6  36141  dfon2lem8  36143  dfon2lem9  36144  dfon2  36145  trer  36681  finminlem  36683  neibastop1  36724  neibastop3  36727  weiunfr  36832  axuntco  36844  regsfromunir1  36905  mh-regprimbi  36910  unbdqndv1  36951  knoppndv  36977  bj-ssbid1ALT  37142  bj-eqs  37153  bj-sb  37167  bj-substw  37205  bj-spcimdv  37385  bj-spcimdvv  37386  bj-csbprc  37400  bj-gabss  37425  bj-elgab  37429  curryset  37436  currysetlem3  37439  bj-cleq  37452  exellimddv  37844  finorwe  37881  wl-motae  38023  wl-cbvalsbi  38054  fin2so  38111  poimirlem17  38141  mblfinlem3  38163  ismblfin  38165  itg2addnc  38178  upixp  38233  mpobi123f  38666  mptbi12f  38670  preuniqval  39000  trcoss  39076  eldisjsim5  39443  prter1  39508  axc11n-16  39567  ax12eq  39570  ax12el  39571  sticksstones22  42790  sbtd  42833  sn-axprlem3  42842  sn-exelALT  42843  ismrcd1  43284  ttac  43618  fnwe2  43635  aomclem6  43641  dfac11  43644  dfac21  43648  hbtlem2  43706  oaun3lem1  43956  cllem0  44147  clss2lem  44192  mptrcllem  44194  iunrelexpmin1  44289  iunrelexpmin2  44293  iunrelexpuztr  44300  dftrcl3  44301  brtrclfv2  44308  dfrtrcl3  44314  psshepw  44369  frege91  44535  frege97  44541  frege109  44553  frege130  44574  grumnudlem  44866  ismnushort  44882  axc11next  44987  pm13.192  44991  pm14.24  45013  gen11  45197  trsspwALT2  45399  snssiALT  45408  sstrALT2  45415  en3lpVD  45425  sspwimp  45498  sspwimpcf  45500  sspwimpALT  45505  ax6e2ndeqALT  45511  ssmapsn  45797  infnsuprnmpt  45830  uzinico  46140  icccncfext  46466  itgsinexplem1  46533  sge0resplit  46985  hspdifhsp  47195  smflimsuplem7  47405  dfatcolem  47854  iccpartdisj  48048  sbcpr  48132  eufsnlem  49467  iscnrm3lem2  49561  functhincfun  50075  termcarweu  50154  setrec2fun  50318  elsetrecslem  50325  setrecsss  50327  setrecsres  50328  0setrec  50330  pgindnf  50342