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

Theorem alimi 1906
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 1905 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1892 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1650
This theorem was proved from axioms:  ax-mp 5  ax-gen 1890  ax-4 1904
This theorem is referenced by:  2alimi  1907  ala1  1908  sylg  1917  19.38  1933  19.26  1968  19.33  1983  alcomiw  2138  alcomiwOLD  2139  hba1w  2142  hbalw  2144  hbal  2200  nfim1  2229  axc4  2307  axc16i  2416  2stdpc4  2444  mobi  2566  mobiOLD  2567  nexmo  2573  nexmoOLD  2574  dfmo  2599  darii  2688  cesare  2695  camestres  2697  festino  2699  baroco  2701  darapti  2713  calemes  2716  fesapo  2724  eqeq1d  2767  ralimi2  3096  rgen2a  3124  ceqsalt  3381  spcgft  3438  rspct  3455  elabgt  3502  reu6  3556  sbciegft  3629  csbeq2  3697  rabss2  3847  csbnestgf  4159  undif4  4197  falseral0  4240  intmin4  4664  dfiin2g  4711  invdisj  4797  disjss3  4810  axrep2  4935  ax6vsep  4947  axnul  4950  csbexg  4955  nfnid  5013  axpr  5063  ssrelrel  5391  idrefOLD  5694  iotanul  6048  iota4  6051  fundif  6118  fv3  6395  zfrep6  7334  dfom3  8761  dfac5  9204  dfac2a  9205  dfac2b  9206  dfac2OLD  9208  kmlem13  9239  zorng  9581  brdom3  9605  brdom4  9607  axpowndlem2  9675  axregnd  9681  axacndlem1  9684  axacndlem2  9685  axacndlem3  9686  axacndlem4  9687  axacnd  9689  ingru  9892  dfnn2  11291  trclfvcotr  14038  prodeq2w  14928  2ndcdisj2  21543  pjnormssi  29486  ssrmo  29790  disjin  29850  disjin2  29851  bnj1172  31520  bnj1174  31522  bnj1176  31524  bnj1523  31590  elpotr  32132  dfon2lem8  32141  distel  32155  hbimtg  32158  bj-gl4lem  33018  bj-alanim  33035  bj-2albi  33036  bj-2exbi  33038  bj-exalim  33050  bj-ssbbi  33062  bj-ssb1a  33072  bj-ssbequ2  33082  bj-ssbid2ALT  33085  bj-sb  33116  bj-hbext  33139  bj-nfalt  33140  bj-nfext  33141  bj-cbv3tb  33149  bj-nfs1t2  33153  bj-stdpc4v  33190  bj-2stdpc4v  33191  bj-axrep2  33222  bj-hbaeb2  33237  bj-equsal1  33243  bj-equsal2  33244  2stdpc5  33248  bj-ceqsalt0  33301  bj-ceqsalt1  33302  bj-bm1.3ii  33454  wl-hbnaev  33735  wl-aleq  33750  wl-lem-nexmo  33777  phpreu  33820  nninfnub  33972  mpt2bi123f  34395  mptbi12f  34399  trcoss  34664  hba1-o  34856  aecom-o  34860  ax12fromc15  34864  hbequid  34868  axc711  34873  axc711toc7  34875  axc711to11  34876  axc5c711  34877  axc5c711toc7  34879  axc5c711to11  34880  equidqe  34881  equid1ALT  34884  axc11nfromc11  34885  axc11n-16  34897  ax12eq  34900  ax12el  34901  ax12indi  34903  dfac11  38312  intimag  38626  intimasn  38627  frege70  38904  pm11.12  39251  2albi  39254  2exbi  39256  pm11.57  39266  pm11.61  39270  axc5c4c711toc7  39281  axc5c4c711to11  39282  axc11next  39283  pm13.192  39287  ralbidar  39324  rexbidar  39325  hbntal  39434  hbimpg  39435  hbexg  39437  ax6e2nd  39439  hbimpgVD  39795  ax6e2eqVD  39798  ax6e2ndVD  39799  ax6e2ndALT  39821  absnsb  41812  rexrsb  41844  setrec1lem2  43107  setrec1lem4  43109
  Copyright terms: Public domain W3C validator