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

Theorem alimi 1729
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 1728 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1714 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-gen 1712  ax-4 1727
This theorem is referenced by:  2alimi  1730  sylg  1739  ala1  1754  19.38  1756  nfnt  1766  19.26  1785  19.33  1800  nfimd  1811  alcomiw  1957  hba1w  1960  hba1wOLD  1961  hbalw  1963  hbal  2022  nfim1  2054  axc4  2114  cbv3hvOLDOLD  2161  axc16i  2309  ax12OLD  2328  2stdpc4  2341  mo2v  2464  eqeq1d  2611  ralimi2  2932  rgen2a  2959  ceqsalt  3200  spcgft  3257  rspct  3274  elabgt  3315  reu6  3361  sbciegft  3432  csbeq2  3502  rabss2  3647  csbnestgf  3947  undif4  3986  ralf0OLD  4030  intmin4  4435  dfiin2g  4483  invdisj  4565  disjss3  4576  axrep2  4695  ax6vsep  4707  axnul  4710  csbexg  4714  nfnid  4817  axpr  4826  ssrelrel  5131  issref  5414  iotanul  5768  iota4  5771  fundif  5834  fv3  6100  zfrep6  7004  dfom3  8404  dfac5  8811  dfac2a  8812  dfac2  8813  kmlem1  8832  kmlem13  8844  zorng  9186  brdom3  9208  brdom4  9210  axpowndlem2  9276  axregnd  9282  axacndlem1  9285  axacndlem2  9286  axacndlem3  9287  axacndlem4  9288  axacnd  9290  ingru  9493  dfnn2  10882  trclfvcotr  13546  prodeq2w  14429  2ndcdisj2  21017  pjnormssi  28204  ssrmo  28511  disjin  28574  disjin2  28575  bnj956  29894  bnj1476  29964  bnj1533  29969  bnj1172  30116  bnj1174  30118  bnj1176  30120  bnj1523  30186  elpotr  30723  dfon2lem8  30732  distel  30746  hbimtg  30749  bj-gl4lem  31545  bj-alanim  31574  bj-2albi  31575  bj-2exbi  31577  bj-alrimhi  31582  bj-ssbbi  31604  bj-ssb1a  31614  bj-ssbequ2  31625  bj-ssbid2ALT  31628  bj-sb  31657  bj-hbext  31681  bj-nfalt  31682  bj-nfext  31683  bj-cbv3tb  31691  bj-nfs1t2  31695  bj-stdpc4v  31735  bj-2stdpc4v  31736  bj-axrep2  31770  bj-hbaeb2  31786  bj-equsal1  31792  bj-equsal2  31793  2stdpc5  31797  bj-eumo0  31811  bj-ceqsalt0  31850  bj-ceqsalt1  31851  wl-hbnaev  32267  wl-aleq  32284  wl-lem-nexmo  32311  phpreu  32346  nninfnub  32500  mpt2bi123f  32924  mptbi12f  32928  hba1-o  32983  aecom-o  32987  ax12fromc15  32991  hbequid  32995  axc711  33000  axc711toc7  33002  axc711to11  33003  axc5c711  33004  axc5c711toc7  33006  axc5c711to11  33007  equidqe  33008  equid1ALT  33011  axc11nfromc11  33012  axc11n-16  33024  ax12eq  33027  ax12el  33028  ax12indi  33030  dfac11  36433  intimag  36750  intimasn  36751  frege70  37030  pm11.12  37379  2albi  37382  2exbi  37384  pm11.57  37394  pm11.61  37398  axc5c4c711toc7  37410  axc5c4c711to11  37411  axc11next  37412  pm13.192  37416  ralbidar  37453  rexbidar  37454  hbntal  37573  hbimpg  37574  hbexg  37576  ax6e2nd  37578  hbimpgVD  37945  ax6e2eqVD  37948  ax6e2ndVD  37949  ax6e2ndALT  37971  rexrsb  39601  falseral0  40092
  Copyright terms: Public domain W3C validator