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  2535  moimdv  2540  mobidv  2543  eubidv  2580  euequ  2591  eqrdv  2728  abbidv  2796  raleqbidvvOLD  3310  elex22  3475  pm13.183  3635  moeq3  3686  sbc2or  3765  sbcthdv  3772  csbied  3901  ssrdv  3955  abssdvOLD  4035  eq0rdv  4373  disj  4416  rabeqsnd  4636  rabsn  4688  dfnfc2  4896  intab  4945  intprg  4948  iuneq12df  4985  dfiin2g  4999  abexd  5283  elALT2  5327  reusv2lem1  5356  reusv2lem2  5357  axprlem3OLD  5386  sbcop1  5451  euotd  5476  ssrelrel  5762  asymref2  6093  dfpo2  6272  iotaval2  6482  iotavalOLD  6488  iota5  6497  iotabidv  6498  funmo  6534  funmoOLD  6535  funco  6559  funun  6565  fununfun  6567  fununi  6594  nfunsn  6903  fvn0ssdmfun  7049  f1oresrab  7102  0mpo0  7475  funoprabg  7513  tfisi  7838  limom  7861  funcnvuni  7911  1stconst  8082  2ndconst  8083  frxp  8108  fnwelem  8113  frxp2  8126  frxp3  8133  frrlem9  8276  seqomlem2  8422  iserd  8700  fsetdmprc0  8831  ssfi  9143  findcard3  9236  findcard3OLD  9237  frfi  9239  fiint  9284  fiintOLD  9285  dffi2  9381  hartogslem1  9502  wdomd  9541  ixpiunwdom  9550  ttrclss  9680  ttrclselem2  9686  rankval3b  9786  fseqenlem2  9985  dfac3  10081  dfac5  10089  dfac2b  10091  dfac8  10096  dfac9  10097  dfacacn  10102  dfac13  10103  kmlem1  10111  kmlem6  10116  kmlem13  10123  fin23lem32  10304  axdc2lem  10408  zornn0g  10465  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2lem12  10602  hargch  10633  alephgch  10634  nqpr  10974  reclem2pr  11008  hashgt23el  14396  cshwsexaOLD  14797  rtrclreclem4  15034  dfrtrcl2  15035  relexpindlem  15036  shftfn  15046  ramub  16991  ramcl  17007  imasaddfnlem  17498  imasvscafn  17507  mrieqv2d  17607  mreexexd  17616  invfun  17733  joinfval  18339  meetfval  18353  mreclatBAD  18529  letsr  18559  efgval  19654  efgi  19656  efgi2  19662  gsumval3lem2  19843  gsumzaddlem  19858  pgpfac1lem5  20018  ringurd  20101  zrinitorngc  20558  zrtermorngc  20559  zrtermoringc  20591  islbs3  21072  lbsextlem4  21078  cssmre  21609  obslbs  21646  mplsubglem  21915  mpllsslem  21916  tgcl  22863  indistopon  22895  ppttop  22901  epttop  22903  mretopd  22986  toponmre  22987  neissex  23021  neiptoptop  23025  lmfun  23275  2ndcdisj  23350  1stccnp  23356  kgentopon  23432  dfac14  23512  ptcnp  23516  uptx  23519  ptrescn  23533  qtoptop2  23593  filconn  23777  filssufilg  23805  rnelfmlem  23846  alexsubALTlem2  23942  cnextfun  23958  utoptop  24129  prdsxmslem2  24424  vitalilem3  25518  mbfposr  25560  mbfinf  25573  i1fd  25589  itg1climres  25622  perfdvf  25811  taylf  26275  addsbdaylem  27930  noseqrdgfn  28207  n0scut  28233  mptelee  28829  upgr1eopALT  29051  upgrspanop  29231  umgrspanop  29232  usgrspanop  29233  cplgrop  29371  umgr2v2enb1  29461  clwwlknon1loop  30034  wlkl0  30303  ex-natded9.26  30355  ex-natded9.26-2  30356  aevdemo  30396  nmcexi  31962  iuneq12daf  32492  iinabrex  32505  abfmpeld  32585  abfmpel  32586  fpwrelmap  32663  ssdifidl  33435  ssmxidl  33452  exsslsb  33599  zarclssn  33870  bnj1143  34787  bnj1379  34827  bnj149  34872  fineqvac  35094  gblacfnacd  35096  vonf1owev  35102  wevgblacfn  35103  loop1cycl  35131  satffunlem1lem1  35396  satffunlem2lem1  35398  prv0  35424  mclsssvlem  35556  ssmclslem  35559  mclsax  35563  mclsind  35564  dfon2lem6  35783  dfon2lem8  35785  dfon2lem9  35786  dfon2  35787  trer  36311  finminlem  36313  neibastop1  36354  neibastop3  36357  weiunfr  36462  unbdqndv1  36503  knoppndv  36529  bj-ssbid1ALT  36660  bj-eqs  36670  bj-sb  36682  bj-substw  36717  bj-nnfbd  36721  bj-spcimdv  36890  bj-spcimdvv  36891  bj-csbprc  36905  bj-gabss  36930  bj-elgab  36934  curryset  36941  currysetlem3  36944  bj-cleq  36957  exellimddv  37340  finorwe  37377  wl-motae  37510  wl-cbvalsbi  37541  fin2so  37608  poimirlem17  37638  mblfinlem3  37660  ismblfin  37662  itg2addnc  37675  upixp  37730  mpobi123f  38163  mptbi12f  38167  trcoss  38480  prter1  38879  axc11n-16  38938  ax12eq  38941  ax12el  38942  sticksstones22  42163  sbtd  42206  sn-axprlem3  42212  sn-exelALT  42213  ismrcd1  42693  ttac  43032  fnwe2  43049  aomclem6  43055  dfac11  43058  dfac21  43062  hbtlem2  43120  oaun3lem1  43370  cllem0  43562  clss2lem  43607  mptrcllem  43609  iunrelexpmin1  43704  iunrelexpmin2  43708  iunrelexpuztr  43715  dftrcl3  43716  brtrclfv2  43723  dfrtrcl3  43729  psshepw  43784  frege91  43950  frege97  43956  frege109  43968  frege130  43989  grumnudlem  44281  ismnushort  44297  axc11next  44402  pm13.192  44406  pm14.24  44428  gen11  44613  trsspwALT2  44815  snssiALT  44824  sstrALT2  44831  en3lpVD  44841  sspwimp  44914  sspwimpcf  44916  sspwimpALT  44921  ax6e2ndeqALT  44927  ssmapsn  45217  infnsuprnmpt  45251  uzinico  45564  icccncfext  45892  itgsinexplem1  45959  sge0resplit  46411  hoidmvlelem1  46600  hspdifhsp  46621  smflimsuplem7  46831  dfatcolem  47260  iccpartdisj  47442  sbcpr  47526  eufsnlem  48833  iscnrm3lem2  48927  functhincfun  49442  termcarweu  49521  setrec2fun  49685  elsetrecslem  49692  setrecsss  49694  setrecsres  49695  0setrec  49697  pgindnf  49709