Theorem alrimiv 1934

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

Syntax hints:   → wi 4  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem is referenced by:  alrimivv  1935  cbvalivw  2014  aevlem0  2063  aev  2066  aev2  2067  stdpc4  2079  sbimdv  2089  sbbidv  2090  elequ2g  2135  cbv3v2  2253  nexmo  2545  moimdv  2550  mobidv  2553  eubidv  2590  euequ  2601  eqrdv  2737  abbidv  2805  elex22  3455  pm13.183  3604  moeq3  3653  sbc2or  3732  sbcthdv  3739  csbied  3867  ssrdv  3921  eq0rdv  4336  rabeqsnd  4602  rabsn  4654  dfnfc2  4861  intab  4909  iuneq12df  4949  elALT2  5299  reusv2lem1  5328  reusv2lem2  5329  axprlem3OLD  5359  sbcop1  5429  euotd  5455  ssrelrel  5740  relimasn  6038  asymref2  6068  dfpo2  6248  iotaval2  6457  iota5  6469  iotabidv  6470  funmo  6502  funco  6526  funun  6532  fununfun  6534  fununi  6561  nfunsn  6867  fvn0ssdmfun  7016  f1oresrab  7070  0mpo0  7440  funoprabg  7478  tfisi  7800  limom  7823  funcnvuni  7873  1stconst  8040  2ndconst  8041  frxp  8067  fnwelem  8072  frxp2  8085  frxp3  8092  frrlem9  8235  seqomlem2  8381  iserd  8661  fsetdmprc0  8793  ssfi  9098  findcard3  9184  frfi  9186  fiint  9228  dffi2  9327  hartogslem1  9448  wdomd  9487  ixpiunwdom  9496  ttrclss  9633  ttrclselem2  9639  rankval3b  9742  fseqenlem2  9939  dfac3  10035  dfac5  10043  dfac2b  10045  dfac8  10050  dfac9  10051  dfacacn  10056  dfac13  10057  kmlem1  10065  kmlem6  10070  kmlem13  10077  fin23lem32  10258  zornn0g  10419  fpwwe2lem10  10555  fpwwe2lem11  10556  fpwwe2lem12  10557  hargch  10588  alephgch  10589  nqpr  10929  reclem2pr  10963  hashgt23el  14378  rtrclreclem4  15015  dfrtrcl2  15016  relexpindlem  15017  shftfn  15027  ramub  16976  ramcl  16992  imasaddfnlem  17484  imasvscafn  17493  mrieqv2d  17597  mreexexd  17606  invfun  17723  joinfval  18329  meetfval  18343  mreclatBAD  18521  letsr  18551  efgval  19684  efgi  19686  efgi2  19692  gsumval3lem2  19873  gsumzaddlem  19888  pgpfac1lem5  20048  ringurd  20158  zrinitorngc  20615  zrtermorngc  20616  zrtermoringc  20648  islbs3  21149  lbsextlem4  21155  cssmre  21669  obslbs  21706  mplsubglem  21974  mpllsslem  21975  tgcl  22953  indistopon  22985  ppttop  22991  epttop  22993  mretopd  23076  toponmre  23077  neissex  23111  neiptoptop  23115  lmfun  23365  2ndcdisj  23440  1stccnp  23446  kgentopon  23522  dfac14  23602  ptcnp  23606  uptx  23609  ptrescn  23623  qtoptop2  23683  filconn  23867  filssufilg  23895  rnelfmlem  23936  alexsubALTlem2  24032  cnextfun  24048  utoptop  24218  prdsxmslem2  24513  vitalilem3  25596  mbfposr  25638  mbfinf  25651  i1fd  25667  itg1climres  25700  perfdvf  25889  taylf  26345  addbdaylem  28028  noseqrdgfn  28317  n0cut  28345  mpteleeOLD  28983  upgr1eopALT  29205  upgrspanop  29385  umgrspanop  29386  usgrspanop  29387  cplgrop  29525  umgr2v2enb1  29614  clwwlknon1loop  30187  wlkl0  30456  ex-natded9.26  30508  ex-natded9.26-2  30509  aevdemo  30549  nmcexi  32116  iuneq12daf  32646  iinabrex  32659  abfmpeld  32747  abfmpel  32748  ssdifidl  33541  ssmxidl  33558  exsslsb  33790  zarclssn  34066  bnj1143  34981  bnj1379  35021  bnj149  35066  rankval4b  35290  r1omhfb  35302  fineqvac  35306  r1omhfbregs  35327  gblacfnacd  35339  vonf1owev  35345  wevgblacfn  35346  loop1cycl  35374  satffunlem1lem1  35639  satffunlem2lem1  35641  prv0  35667  mclsssvlem  35799  ssmclslem  35802  mclsax  35806  mclsind  35807  dfon2lem6  36023  dfon2lem8  36025  dfon2lem9  36026  dfon2  36027  trer  36553  finminlem  36555  neibastop1  36596  neibastop3  36599  weiunfr  36704  axuntco  36716  regsfromunir1  36777  mh-regprimbi  36782  unbdqndv1  36823  knoppndv  36849  bj-ssbid1ALT  37014  bj-eqs  37025  bj-sb  37039  bj-substw  37077  bj-spcimdv  37257  bj-spcimdvv  37258  bj-csbprc  37272  bj-gabss  37297  bj-elgab  37301  curryset  37308  currysetlem3  37311  bj-cleq  37324  exellimddv  37716  finorwe  37753  wl-motae  37895  wl-cbvalsbi  37926  fin2so  37983  poimirlem17  38013  mblfinlem3  38035  ismblfin  38037  itg2addnc  38050  upixp  38105  mpobi123f  38538  mptbi12f  38542  preuniqval  38872  trcoss  38948  eldisjsim5  39315  prter1  39380  axc11n-16  39439  ax12eq  39442  ax12el  39443  sticksstones22  42662  sbtd  42705  sn-axprlem3  42714  sn-exelALT  42715  ismrcd1  43156  ttac  43490  fnwe2  43507  aomclem6  43513  dfac11  43516  dfac21  43520  hbtlem2  43578  oaun3lem1  43828  cllem0  44019  clss2lem  44064  mptrcllem  44066  iunrelexpmin1  44161  iunrelexpmin2  44165  iunrelexpuztr  44172  dftrcl3  44173  brtrclfv2  44180  dfrtrcl3  44186  psshepw  44241  frege91  44407  frege97  44413  frege109  44425  frege130  44446  grumnudlem  44738  ismnushort  44754  axc11next  44859  pm13.192  44863  pm14.24  44885  gen11  45069  trsspwALT2  45271  snssiALT  45280  sstrALT2  45287  en3lpVD  45297  sspwimp  45370  sspwimpcf  45372  sspwimpALT  45377  ax6e2ndeqALT  45383  ssmapsn  45669  infnsuprnmpt  45702  uzinico  46012  icccncfext  46338  itgsinexplem1  46405  sge0resplit  46857  hspdifhsp  47067  smflimsuplem7  47277  dfatcolem  47726  iccpartdisj  47920  sbcpr  48004  eufsnlem  49339  iscnrm3lem2  49433  functhincfun  49947  termcarweu  50026  setrec2fun  50190  elsetrecslem  50197  setrecsss  50199  setrecsres  50200  0setrec  50202  pgindnf  50214