MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alimi Structured version   Visualization version   GIF version

Theorem alimi 1884
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)
Hypothesis
Ref Expression
alimi.1 (𝜑𝜓)
Assertion
Ref Expression
alimi (∀𝑥𝜑 → ∀𝑥𝜓)

Proof of Theorem alimi
StepHypRef Expression
1 alim 1883 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1869 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1626
This theorem was proved from axioms:  ax-mp 5  ax-gen 1867  ax-4 1882
This theorem is referenced by:  2alimi  1885  ala1  1886  sylg  1895  19.38  1911  nfntOLDOLD  1928  19.26  1943  19.33  1957  nfimdOLDOLD  1969  alcomiw  2118  hba1w  2121  hba1wOLD  2122  hbalw  2124  hbal  2181  nfim1  2210  axc4  2273  axc16i  2458  ax12OLD  2477  2stdpc4  2487  mo2v  2610  eqeq1d  2758  ralimi2  3083  rgen2a  3111  ceqsalt  3364  spcgft  3421  rspct  3438  elabgt  3483  reu6  3532  sbciegft  3603  csbeq2  3674  rabss2  3822  csbnestgf  4135  undif4  4175  ralf0OLD  4219  falseral0  4221  intmin4  4654  dfiin2g  4701  invdisj  4786  disjss3  4799  axrep2  4921  ax6vsep  4933  axnul  4936  csbexg  4940  nfnid  5042  axpr  5050  ssrelrel  5373  issref  5663  iotanul  6023  iota4  6026  fundif  6092  fv3  6363  zfrep6  7295  dfom3  8713  dfac5  9137  dfac2a  9138  dfac2b  9139  dfac2OLD  9141  kmlem13  9172  zorng  9514  brdom3  9538  brdom4  9540  axpowndlem2  9608  axregnd  9614  axacndlem1  9617  axacndlem2  9618  axacndlem3  9619  axacndlem4  9620  axacnd  9622  ingru  9825  dfnn2  11221  trclfvcotr  13945  prodeq2w  14837  2ndcdisj2  21458  pjnormssi  29332  ssrmo  29638  disjin  29702  disjin2  29703  bnj1172  31372  bnj1174  31374  bnj1176  31376  bnj1523  31442  elpotr  31987  dfon2lem8  31996  distel  32010  hbimtg  32013  bj-gl4lem  32881  bj-alanim  32898  bj-2albi  32899  bj-2exbi  32901  bj-alrimhi  32906  bj-exalim  32913  bj-ssbbi  32924  bj-ssb1a  32934  bj-ssbequ2  32945  bj-ssbid2ALT  32948  bj-sb  32979  bj-hbext  33003  bj-nfalt  33004  bj-nfext  33005  bj-cbv3tb  33013  bj-nfs1t2  33017  bj-stdpc4v  33056  bj-2stdpc4v  33057  bj-axrep2  33091  bj-hbaeb2  33107  bj-equsal1  33113  bj-equsal2  33114  2stdpc5  33118  bj-eumo0  33132  bj-ceqsalt0  33175  bj-ceqsalt1  33176  wl-hbnaev  33614  wl-aleq  33631  wl-lem-nexmo  33658  phpreu  33702  nninfnub  33856  mpt2bi123f  34280  mptbi12f  34284  trcoss  34551  hba1-o  34682  aecom-o  34686  ax12fromc15  34690  hbequid  34694  axc711  34699  axc711toc7  34701  axc711to11  34702  axc5c711  34703  axc5c711toc7  34705  axc5c711to11  34706  equidqe  34707  equid1ALT  34710  axc11nfromc11  34711  axc11n-16  34723  ax12eq  34726  ax12el  34727  ax12indi  34729  dfac11  38130  intimag  38446  intimasn  38447  frege70  38725  pm11.12  39072  2albi  39075  2exbi  39077  pm11.57  39087  pm11.61  39091  axc5c4c711toc7  39103  axc5c4c711to11  39104  axc11next  39105  pm13.192  39109  ralbidar  39147  rexbidar  39148  hbntal  39267  hbimpg  39268  hbexg  39270  ax6e2nd  39272  hbimpgVD  39635  ax6e2eqVD  39638  ax6e2ndVD  39639  ax6e2ndALT  39661  rexrsb  41671  setrec1lem2  42941  setrec1lem4  42943
  Copyright terms: Public domain W3C validator