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

Theorem alimi 1736
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 1735 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1721 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-gen 1719  ax-4 1734
This theorem is referenced by:  2alimi  1737  ala1  1738  sylg  1747  19.38  1763  nfntOLDOLD  1780  19.26  1795  19.33  1809  nfimdOLDOLD  1821  alcomiw  1968  hba1w  1971  hba1wOLD  1972  hbalw  1974  hbal  2033  nfim1  2065  axc4  2126  cbv3hvOLDOLD  2173  axc16i  2321  ax12OLD  2340  2stdpc4  2353  mo2v  2476  eqeq1d  2623  ralimi2  2945  rgen2a  2973  ceqsalt  3218  spcgft  3275  rspct  3292  elabgt  3335  reu6  3382  sbciegft  3453  csbeq2  3523  rabss2  3670  csbnestgf  3974  undif4  4013  ralf0OLD  4057  falseral0  4059  intmin4  4478  dfiin2g  4526  invdisj  4611  disjss3  4622  axrep2  4743  ax6vsep  4755  axnul  4758  csbexg  4762  nfnid  4867  axpr  4876  ssrelrel  5191  issref  5478  iotanul  5835  iota4  5838  fundif  5903  fv3  6173  zfrep6  7096  dfom3  8504  dfac5  8911  dfac2a  8912  dfac2  8913  kmlem13  8944  zorng  9286  brdom3  9310  brdom4  9312  axpowndlem2  9380  axregnd  9386  axacndlem1  9389  axacndlem2  9390  axacndlem3  9391  axacndlem4  9392  axacnd  9394  ingru  9597  dfnn2  10993  trclfvcotr  13700  prodeq2w  14586  2ndcdisj2  21200  pjnormssi  28915  ssrmo  29223  disjin  29285  disjin2  29286  bnj1172  30830  bnj1174  30832  bnj1176  30834  bnj1523  30900  elpotr  31440  dfon2lem8  31449  distel  31463  hbimtg  31466  bj-gl4lem  32274  bj-alanim  32291  bj-2albi  32292  bj-2exbi  32294  bj-alrimhi  32299  bj-exalim  32306  bj-ssbbi  32317  bj-ssb1a  32327  bj-ssbequ2  32338  bj-ssbid2ALT  32341  bj-sb  32372  bj-hbext  32396  bj-nfalt  32397  bj-nfext  32398  bj-cbv3tb  32406  bj-nfs1t2  32410  bj-stdpc4v  32450  bj-2stdpc4v  32451  bj-axrep2  32485  bj-hbaeb2  32501  bj-equsal1  32507  bj-equsal2  32508  2stdpc5  32512  bj-eumo0  32526  bj-ceqsalt0  32573  bj-ceqsalt1  32574  wl-hbnaev  32976  wl-aleq  32993  wl-lem-nexmo  33020  phpreu  33064  nninfnub  33218  mpt2bi123f  33642  mptbi12f  33646  hba1-o  33701  aecom-o  33705  ax12fromc15  33709  hbequid  33713  axc711  33718  axc711toc7  33720  axc711to11  33721  axc5c711  33722  axc5c711toc7  33724  axc5c711to11  33725  equidqe  33726  equid1ALT  33729  axc11nfromc11  33730  axc11n-16  33742  ax12eq  33745  ax12el  33746  ax12indi  33748  dfac11  37151  intimag  37468  intimasn  37469  frege70  37748  pm11.12  38095  2albi  38098  2exbi  38100  pm11.57  38110  pm11.61  38114  axc5c4c711toc7  38126  axc5c4c711to11  38127  axc11next  38128  pm13.192  38132  ralbidar  38170  rexbidar  38171  hbntal  38290  hbimpg  38291  hbexg  38293  ax6e2nd  38295  hbimpgVD  38662  ax6e2eqVD  38665  ax6e2ndVD  38666  ax6e2ndALT  38688  rexrsb  40503  setrec1lem2  41758  setrec1lem4  41760
  Copyright terms: Public domain W3C validator