Theorem alrimiv 1927

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  alrimivv  1928  cbvalivw  2007  aevlem0  2055  aev  2058  aev2  2059  stdpc4  2069  sbimdv  2079  sbbidv  2080  elequ2g  2125  cbv3v2  2242  nexmo  2534  moimdv  2539  mobidv  2542  eubidv  2579  euequ  2590  eqrdv  2727  abbidv  2795  raleqbidvvOLD  3308  elex22  3472  pm13.183  3632  moeq3  3683  sbc2or  3762  sbcthdv  3769  csbied  3898  ssrdv  3952  abssdvOLD  4032  eq0rdv  4370  disj  4413  rabeqsnd  4633  rabsn  4685  dfnfc2  4893  intab  4942  intprg  4945  iuneq12df  4982  dfiin2g  4996  abexd  5280  elALT2  5324  reusv2lem1  5353  reusv2lem2  5354  axprlem3OLD  5383  sbcop1  5448  euotd  5473  ssrelrel  5759  asymref2  6090  dfpo2  6269  iotaval2  6479  iotavalOLD  6485  iota5  6494  iotabidv  6495  funmo  6531  funmoOLD  6532  funco  6556  funun  6562  fununfun  6564  fununi  6591  nfunsn  6900  fvn0ssdmfun  7046  f1oresrab  7099  0mpo0  7472  funoprabg  7510  tfisi  7835  limom  7858  funcnvuni  7908  1stconst  8079  2ndconst  8080  frxp  8105  fnwelem  8110  frxp2  8123  frxp3  8130  frrlem9  8273  seqomlem2  8419  iserd  8697  fsetdmprc0  8828  ssfi  9137  findcard3  9229  findcard3OLD  9230  frfi  9232  fiint  9277  fiintOLD  9278  dffi2  9374  hartogslem1  9495  wdomd  9534  ixpiunwdom  9543  ttrclss  9673  ttrclselem2  9679  rankval3b  9779  fseqenlem2  9978  dfac3  10074  dfac5  10082  dfac2b  10084  dfac8  10089  dfac9  10090  dfacacn  10095  dfac13  10096  kmlem1  10104  kmlem6  10109  kmlem13  10116  fin23lem32  10297  axdc2lem  10401  zornn0g  10458  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  hargch  10626  alephgch  10627  nqpr  10967  reclem2pr  11001  hashgt23el  14389  cshwsexaOLD  14790  rtrclreclem4  15027  dfrtrcl2  15028  relexpindlem  15029  shftfn  15039  ramub  16984  ramcl  17000  imasaddfnlem  17491  imasvscafn  17500  mrieqv2d  17600  mreexexd  17609  invfun  17726  joinfval  18332  meetfval  18346  mreclatBAD  18522  letsr  18552  efgval  19647  efgi  19649  efgi2  19655  gsumval3lem2  19836  gsumzaddlem  19851  pgpfac1lem5  20011  ringurd  20094  zrinitorngc  20551  zrtermorngc  20552  zrtermoringc  20584  islbs3  21065  lbsextlem4  21071  cssmre  21602  obslbs  21639  mplsubglem  21908  mpllsslem  21909  tgcl  22856  indistopon  22888  ppttop  22894  epttop  22896  mretopd  22979  toponmre  22980  neissex  23014  neiptoptop  23018  lmfun  23268  2ndcdisj  23343  1stccnp  23349  kgentopon  23425  dfac14  23505  ptcnp  23509  uptx  23512  ptrescn  23526  qtoptop2  23586  filconn  23770  filssufilg  23798  rnelfmlem  23839  alexsubALTlem2  23935  cnextfun  23951  utoptop  24122  prdsxmslem2  24417  vitalilem3  25511  mbfposr  25553  mbfinf  25566  i1fd  25582  itg1climres  25615  perfdvf  25804  taylf  26268  addsbdaylem  27923  noseqrdgfn  28200  n0scut  28226  mptelee  28822  upgr1eopALT  29044  upgrspanop  29224  umgrspanop  29225  usgrspanop  29226  cplgrop  29364  umgr2v2enb1  29454  clwwlknon1loop  30027  wlkl0  30296  ex-natded9.26  30348  ex-natded9.26-2  30349  aevdemo  30389  nmcexi  31955  iuneq12daf  32485  iinabrex  32498  abfmpeld  32578  abfmpel  32579  fpwrelmap  32656  ssdifidl  33428  ssmxidl  33445  exsslsb  33592  zarclssn  33863  bnj1143  34780  bnj1379  34820  bnj149  34865  fineqvac  35087  gblacfnacd  35089  vonf1owev  35095  wevgblacfn  35096  loop1cycl  35124  satffunlem1lem1  35389  satffunlem2lem1  35391  prv0  35417  mclsssvlem  35549  ssmclslem  35552  mclsax  35556  mclsind  35557  dfon2lem6  35776  dfon2lem8  35778  dfon2lem9  35779  dfon2  35780  trer  36304  finminlem  36306  neibastop1  36347  neibastop3  36350  weiunfr  36455  unbdqndv1  36496  knoppndv  36522  bj-ssbid1ALT  36653  bj-eqs  36663  bj-sb  36675  bj-substw  36710  bj-nnfbd  36714  bj-spcimdv  36883  bj-spcimdvv  36884  bj-csbprc  36898  bj-gabss  36923  bj-elgab  36927  curryset  36934  currysetlem3  36937  bj-cleq  36950  exellimddv  37333  finorwe  37370  wl-motae  37503  wl-cbvalsbi  37534  fin2so  37601  poimirlem17  37631  mblfinlem3  37653  ismblfin  37655  itg2addnc  37668  upixp  37723  mpobi123f  38156  mptbi12f  38160  trcoss  38473  prter1  38872  axc11n-16  38931  ax12eq  38934  ax12el  38935  sticksstones22  42156  sbtd  42199  sn-axprlem3  42205  sn-exelALT  42206  ismrcd1  42686  ttac  43025  fnwe2  43042  aomclem6  43048  dfac11  43051  dfac21  43055  hbtlem2  43113  oaun3lem1  43363  cllem0  43555  clss2lem  43600  mptrcllem  43602  iunrelexpmin1  43697  iunrelexpmin2  43701  iunrelexpuztr  43708  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  psshepw  43777  frege91  43943  frege97  43949  frege109  43961  frege130  43982  grumnudlem  44274  ismnushort  44290  axc11next  44395  pm13.192  44399  pm14.24  44421  gen11  44606  trsspwALT2  44808  snssiALT  44817  sstrALT2  44824  en3lpVD  44834  sspwimp  44907  sspwimpcf  44909  sspwimpALT  44914  ax6e2ndeqALT  44920  ssmapsn  45210  infnsuprnmpt  45244  uzinico  45557  icccncfext  45885  itgsinexplem1  45952  sge0resplit  46404  hoidmvlelem1  46593  hspdifhsp  46614  smflimsuplem7  46824  dfatcolem  47256  iccpartdisj  47438  sbcpr  47522  eufsnlem  48829  iscnrm3lem2  48923  functhincfun  49438  termcarweu  49517  setrec2fun  49681  elsetrecslem  49688  setrecsss  49690  setrecsres  49691  0setrec  49693  pgindnf  49705