Theorem alrimiv 1927

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2207 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  2006  aevlem0  2054  aev  2057  aev2  2058  stdpc4  2068  sbimdv  2078  sbbidv  2079  elequ2g  2124  cbv3v2  2241  nexmo  2540  moimdv  2545  mobidv  2548  eubidv  2585  euequ  2596  eqrdv  2733  abbidv  2801  raleqbidvvOLD  3314  elex2OLD  3484  elex22  3485  pm13.183  3645  moeq3  3695  sbc2or  3774  sbcthdv  3781  csbied  3910  ssrdv  3964  abssdvOLD  4044  eq0rdv  4382  disj  4425  rabeqsnd  4645  rabsn  4697  dfnfc2  4905  intab  4954  intprg  4957  iuneq12df  4994  dfiin2g  5008  abexd  5295  elALT2  5339  reusv2lem1  5368  reusv2lem2  5369  axprlem3OLD  5398  sbcop1  5463  euotd  5488  ssrelrel  5775  asymref2  6106  dfpo2  6285  iotaval2  6499  iotavalOLD  6505  iota5  6514  iotabidv  6515  funmo  6551  funmoOLD  6552  funco  6576  funun  6582  fununfun  6584  fununi  6611  nfunsn  6918  fvn0ssdmfun  7064  f1oresrab  7117  0mpo0  7490  funoprabg  7528  tfisi  7854  limom  7877  funcnvuni  7928  1stconst  8099  2ndconst  8100  frxp  8125  fnwelem  8130  frxp2  8143  frxp3  8150  frrlem9  8293  seqomlem2  8465  iserd  8745  fsetdmprc0  8869  ssfi  9187  findcard3  9290  findcard3OLD  9291  frfi  9293  fiint  9338  fiintOLD  9339  dffi2  9435  hartogslem1  9556  wdomd  9595  ixpiunwdom  9604  ttrclss  9734  ttrclselem2  9740  rankval3b  9840  fseqenlem2  10039  dfac3  10135  dfac5  10143  dfac2b  10145  dfac8  10150  dfac9  10151  dfacacn  10156  dfac13  10157  kmlem1  10165  kmlem6  10170  kmlem13  10177  fin23lem32  10358  axdc2lem  10462  zornn0g  10519  fpwwe2lem10  10654  fpwwe2lem11  10655  fpwwe2lem12  10656  hargch  10687  alephgch  10688  nqpr  11028  reclem2pr  11062  hashgt23el  14442  cshwsexaOLD  14843  rtrclreclem4  15080  dfrtrcl2  15081  relexpindlem  15082  shftfn  15092  ramub  17033  ramcl  17049  imasaddfnlem  17542  imasvscafn  17551  mrieqv2d  17651  mreexexd  17660  invfun  17777  joinfval  18383  meetfval  18397  mreclatBAD  18573  letsr  18603  efgval  19698  efgi  19700  efgi2  19706  gsumval3lem2  19887  gsumzaddlem  19902  pgpfac1lem5  20062  ringurd  20145  zrinitorngc  20602  zrtermorngc  20603  zrtermoringc  20635  islbs3  21116  lbsextlem4  21122  cssmre  21653  obslbs  21690  mplsubglem  21959  mpllsslem  21960  tgcl  22907  indistopon  22939  ppttop  22945  epttop  22947  mretopd  23030  toponmre  23031  neissex  23065  neiptoptop  23069  lmfun  23319  2ndcdisj  23394  1stccnp  23400  kgentopon  23476  dfac14  23556  ptcnp  23560  uptx  23563  ptrescn  23577  qtoptop2  23637  filconn  23821  filssufilg  23849  rnelfmlem  23890  alexsubALTlem2  23986  cnextfun  24002  utoptop  24173  prdsxmslem2  24468  vitalilem3  25563  mbfposr  25605  mbfinf  25618  i1fd  25634  itg1climres  25667  perfdvf  25856  taylf  26320  addsbdaylem  27975  noseqrdgfn  28252  n0scut  28278  mptelee  28874  upgr1eopALT  29096  upgrspanop  29276  umgrspanop  29277  usgrspanop  29278  cplgrop  29416  umgr2v2enb1  29506  clwwlknon1loop  30079  wlkl0  30348  ex-natded9.26  30400  ex-natded9.26-2  30401  aevdemo  30441  nmcexi  32007  iuneq12daf  32537  iinabrex  32550  abfmpeld  32632  abfmpel  32633  fpwrelmap  32710  ssdifidl  33472  ssmxidl  33489  exsslsb  33636  zarclssn  33904  bnj1143  34821  bnj1379  34861  bnj149  34906  fineqvac  35128  gblacfnacd  35130  wevgblacfn  35131  loop1cycl  35159  satffunlem1lem1  35424  satffunlem2lem1  35426  prv0  35452  mclsssvlem  35584  ssmclslem  35587  mclsax  35591  mclsind  35592  dfon2lem6  35806  dfon2lem8  35808  dfon2lem9  35809  dfon2  35810  trer  36334  finminlem  36336  neibastop1  36377  neibastop3  36380  weiunfr  36485  unbdqndv1  36526  knoppndv  36552  bj-ssbid1ALT  36683  bj-eqs  36693  bj-sb  36705  bj-substw  36740  bj-nnfbd  36744  bj-spcimdv  36913  bj-spcimdvv  36914  bj-csbprc  36928  bj-gabss  36953  bj-elgab  36957  curryset  36964  currysetlem3  36967  bj-cleq  36980  exellimddv  37363  finorwe  37400  wl-motae  37533  wl-cbvalsbi  37564  fin2so  37631  poimirlem17  37661  mblfinlem3  37683  ismblfin  37685  itg2addnc  37698  upixp  37753  mpobi123f  38186  mptbi12f  38190  trcoss  38500  prter1  38897  axc11n-16  38956  ax12eq  38959  ax12el  38960  sticksstones22  42181  sbtd  42262  sn-axprlem3  42268  sn-exelALT  42269  ismrcd1  42721  ttac  43060  fnwe2  43077  aomclem6  43083  dfac11  43086  dfac21  43090  hbtlem2  43148  oaun3lem1  43398  cllem0  43590  clss2lem  43635  mptrcllem  43637  iunrelexpmin1  43732  iunrelexpmin2  43736  iunrelexpuztr  43743  dftrcl3  43744  brtrclfv2  43751  dfrtrcl3  43757  psshepw  43812  frege91  43978  frege97  43984  frege109  43996  frege130  44017  grumnudlem  44309  ismnushort  44325  axc11next  44430  pm13.192  44434  pm14.24  44456  gen11  44641  trsspwALT2  44843  snssiALT  44852  sstrALT2  44859  en3lpVD  44869  sspwimp  44942  sspwimpcf  44944  sspwimpALT  44949  ax6e2ndeqALT  44955  ssmapsn  45240  infnsuprnmpt  45274  uzinico  45588  icccncfext  45916  itgsinexplem1  45983  sge0resplit  46435  hoidmvlelem1  46624  hspdifhsp  46645  smflimsuplem7  46855  dfatcolem  47284  iccpartdisj  47451  sbcpr  47535  eufsnlem  48819  iscnrm3lem2  48909  functhincfun  49335  termcarweu  49413  setrec2fun  49556  elsetrecslem  49563  setrecsss  49565  setrecsres  49566  0setrec  49568  pgindnf  49580