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

Theorem alimi 1813
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 1812 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1799 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-gen 1797  ax-4 1811
This theorem is referenced by:  2alimi  1814  ala1  1815  sylg  1824  19.38  1840  19.26  1871  19.33  1885  alcomiw  2050  alcomiwOLD  2051  hba1w  2054  hbalw  2056  naev2  2066  2stdpc4  2075  spsbbi  2078  hbal  2172  hbsbw  2174  nfim1  2198  sbequ2OLD  2250  axc4  2332  axc16i  2450  sb4a  2501  dfmoeu  2597  nexmo  2602  moimi  2606  eu6  2637  darii  2730  cesare  2737  camestres  2738  festino  2739  baroco  2741  darapti  2749  calemes  2752  fesapo  2756  eqeq1d  2803  ralimi2  3128  rgen2a  3196  ceqsalt  3477  spcgft  3538  rspct  3560  elabgt  3612  reu6  3668  sbciegft  3759  csbeq2  3836  ssrmof  3983  rabss2  4008  csbnestgfw  4330  csbnestgf  4335  undif4  4377  falseral0  4420  intmin4  4870  dfiin2g  4922  invdisj  5017  disjss3  5032  axrep2  5160  ax6vsep  5174  axnul  5176  csbexg  5181  nfnid  5244  axprALT  5291  axprlem1  5292  axprlem4  5295  axprlem5  5296  axpr  5297  ssrelrel  5637  iresn0n0  5894  iotanul  6306  iota4  6309  fundif  6377  fv3  6667  zfrep6  7642  dfom3  9098  dfac5  9543  dfac2a  9544  dfac2b  9545  kmlem13  9577  zorng  9919  brdom3  9943  brdom4  9945  axpowndlem2  10013  axregnd  10019  axacndlem1  10022  axacndlem2  10023  axacndlem3  10024  axacndlem4  10025  axacnd  10027  ingru  10230  dfnn2  11642  trclfvcotr  14364  prodeq2w  15262  2ndcdisj2  22066  pjnormssi  29955  disjin  30353  disjin2  30354  bnj1172  32387  bnj1174  32389  bnj1176  32391  bnj1523  32457  elpotr  33140  dfon2lem8  33149  distel  33162  hbimtg  33165  bj-gl4  34043  bj-alanim  34060  bj-2albi  34061  bj-exalim  34079  bj-cbvalimt  34086  bj-cbveximt  34087  bj-eximALT  34088  bj-aleximiALT  34089  bj-ssbid2ALT  34110  bj-sb  34135  bj-hbext  34158  bj-nfalt  34159  bj-nfext  34160  bj-nnfalt  34211  bj-nnfext  34212  bj-cbv3tb  34225  bj-nfs1t2  34229  bj-hbaeb2  34257  bj-equsal1  34263  bj-equsal2  34264  2stdpc5  34268  bj-ceqsalt0  34325  bj-ceqsalt1  34326  bj-bm1.3ii  34482  exrecfnlem  34797  wl-moae  34920  wl-aleq  34939  wl-lem-nexmo  34967  wl-axc11rc11  34979  phpreu  35040  nninfnub  35188  mpobi123f  35599  trcoss  35881  hba1-o  36192  aecom-o  36196  ax12fromc15  36200  hbequid  36204  axc711  36209  axc711toc7  36211  axc711to11  36212  axc5c711  36213  axc5c711toc7  36215  axc5c711to11  36216  equidqe  36217  equid1ALT  36220  axc11nfromc11  36221  axc11n-16  36233  ax12eq  36236  ax12el  36237  ax12indi  36239  dfac11  40003  intimag  40354  intimasn  40355  frege70  40631  pm11.12  41076  2albi  41079  2exbi  41081  pm11.57  41090  pm11.61  41094  axc5c4c711toc7  41105  axc5c4c711to11  41106  axc11next  41107  pm13.192  41111  ralbidar  41146  rexbidar  41147  hbntal  41256  hbimpg  41257  hbexg  41259  ax6e2nd  41261  hbimpgVD  41607  ax6e2eqVD  41610  ax6e2ndVD  41611  ax6e2ndALT  41633  absnsb  43616  rexrsb  43652  ichal  43980  setrec1lem2  45215  setrec1lem4  45217
  Copyright terms: Public domain W3C validator