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

Theorem alimi 1730
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 1729 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1715 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-gen 1713  ax-4 1728
This theorem is referenced by:  2alimi  1731  sylg  1740  ala1  1755  19.38  1757  nfnt  1767  19.26  1786  19.33  1801  nfimd  1812  alcomiw  1958  hba1w  1961  hba1wOLD  1962  hbalw  1964  hbal  2023  nfim1  2055  axc4  2115  cbv3hvOLDOLD  2162  axc16i  2310  ax12OLD  2329  2stdpc4  2342  mo2v  2465  eqeq1d  2612  ralimi2  2933  rgen2a  2960  ceqsalt  3201  spcgft  3258  rspct  3275  elabgt  3316  reu6  3362  sbciegft  3433  csbeq2  3503  rabss2  3648  csbnestgf  3948  undif4  3987  ralf0OLD  4031  intmin4  4441  dfiin2g  4489  invdisj  4571  disjss3  4582  axrep2  4701  ax6vsep  4713  axnul  4716  csbexg  4720  nfnid  4823  axpr  4832  ssrelrel  5143  issref  5428  iotanul  5783  iota4  5786  fundif  5849  fv3  6116  zfrep6  7027  dfom3  8427  dfac5  8834  dfac2a  8835  dfac2  8836  kmlem1  8855  kmlem13  8867  zorng  9209  brdom3  9231  brdom4  9233  axpowndlem2  9299  axregnd  9305  axacndlem1  9308  axacndlem2  9309  axacndlem3  9310  axacndlem4  9311  axacnd  9313  ingru  9516  dfnn2  10910  trclfvcotr  13598  prodeq2w  14481  2ndcdisj2  21070  pjnormssi  28411  ssrmo  28718  disjin  28781  disjin2  28782  bnj956  30101  bnj1476  30171  bnj1533  30176  bnj1172  30323  bnj1174  30325  bnj1176  30327  bnj1523  30393  elpotr  30930  dfon2lem8  30939  distel  30953  hbimtg  30956  bj-gl4lem  31752  bj-alanim  31781  bj-2albi  31782  bj-2exbi  31784  bj-alrimhi  31789  bj-ssbbi  31811  bj-ssb1a  31821  bj-ssbequ2  31832  bj-ssbid2ALT  31835  bj-sb  31864  bj-hbext  31888  bj-nfalt  31889  bj-nfext  31890  bj-cbv3tb  31898  bj-nfs1t2  31902  bj-stdpc4v  31942  bj-2stdpc4v  31943  bj-axrep2  31977  bj-hbaeb2  31993  bj-equsal1  31999  bj-equsal2  32000  2stdpc5  32004  bj-eumo0  32018  bj-ceqsalt0  32067  bj-ceqsalt1  32068  wl-hbnaev  32484  wl-aleq  32501  wl-lem-nexmo  32528  phpreu  32563  nninfnub  32717  mpt2bi123f  33141  mptbi12f  33145  hba1-o  33200  aecom-o  33204  ax12fromc15  33208  hbequid  33212  axc711  33217  axc711toc7  33219  axc711to11  33220  axc5c711  33221  axc5c711toc7  33223  axc5c711to11  33224  equidqe  33225  equid1ALT  33228  axc11nfromc11  33229  axc11n-16  33241  ax12eq  33244  ax12el  33245  ax12indi  33247  dfac11  36650  intimag  36967  intimasn  36968  frege70  37247  pm11.12  37596  2albi  37599  2exbi  37601  pm11.57  37611  pm11.61  37615  axc5c4c711toc7  37627  axc5c4c711to11  37628  axc11next  37629  pm13.192  37633  ralbidar  37670  rexbidar  37671  hbntal  37790  hbimpg  37791  hbexg  37793  ax6e2nd  37795  hbimpgVD  38162  ax6e2eqVD  38165  ax6e2ndVD  38166  ax6e2ndALT  38188  rexrsb  39818  falseral0  40308  setrec1lem2  42234  setrec1lem4  42236
  Copyright terms: Public domain W3C validator