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

Theorem alimi 1779
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 1778 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2 alimi.1 . 2 (𝜑𝜓)
31, 2mpg 1764 1 (∀𝑥𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-gen 1762  ax-4 1777
This theorem is referenced by:  2alimi  1780  ala1  1781  sylg  1790  19.38  1806  nfntOLDOLD  1823  19.26  1838  19.33  1852  nfimdOLDOLD  1864  alcomiw  2013  hba1w  2016  hba1wOLD  2017  hbalw  2019  hbal  2076  nfim1  2105  axc4  2168  axc16i  2353  ax12OLD  2372  2stdpc4  2382  mo2v  2505  eqeq1d  2653  ralimi2  2978  rgen2a  3006  ceqsalt  3259  spcgft  3316  rspct  3333  elabgt  3379  reu6  3428  sbciegft  3499  csbeq2  3570  rabss2  3718  csbnestgf  4029  undif4  4068  ralf0OLD  4112  falseral0  4114  intmin4  4538  dfiin2g  4585  invdisj  4670  disjss3  4684  axrep2  4806  ax6vsep  4818  axnul  4821  csbexg  4825  nfnid  4927  axpr  4935  ssrelrel  5254  issref  5544  iotanul  5904  iota4  5907  fundif  5973  fv3  6244  zfrep6  7176  dfom3  8582  dfac5  8989  dfac2a  8990  dfac2  8991  kmlem13  9022  zorng  9364  brdom3  9388  brdom4  9390  axpowndlem2  9458  axregnd  9464  axacndlem1  9467  axacndlem2  9468  axacndlem3  9469  axacndlem4  9470  axacnd  9472  ingru  9675  dfnn2  11071  trclfvcotr  13794  prodeq2w  14686  2ndcdisj2  21308  pjnormssi  29155  ssrmo  29461  disjin  29525  disjin2  29526  bnj1172  31195  bnj1174  31197  bnj1176  31199  bnj1523  31265  elpotr  31810  dfon2lem8  31819  distel  31833  hbimtg  31836  bj-gl4lem  32704  bj-alanim  32721  bj-2albi  32722  bj-2exbi  32724  bj-alrimhi  32729  bj-exalim  32736  bj-ssbbi  32747  bj-ssb1a  32757  bj-ssbequ2  32768  bj-ssbid2ALT  32771  bj-sb  32802  bj-hbext  32826  bj-nfalt  32827  bj-nfext  32828  bj-cbv3tb  32836  bj-nfs1t2  32840  bj-stdpc4v  32879  bj-2stdpc4v  32880  bj-axrep2  32914  bj-hbaeb2  32930  bj-equsal1  32936  bj-equsal2  32937  2stdpc5  32941  bj-eumo0  32955  bj-ceqsalt0  32998  bj-ceqsalt1  32999  wl-hbnaev  33435  wl-aleq  33452  wl-lem-nexmo  33479  phpreu  33523  nninfnub  33677  mpt2bi123f  34101  mptbi12f  34105  trcoss  34372  hba1-o  34501  aecom-o  34505  ax12fromc15  34509  hbequid  34513  axc711  34518  axc711toc7  34520  axc711to11  34521  axc5c711  34522  axc5c711toc7  34524  axc5c711to11  34525  equidqe  34526  equid1ALT  34529  axc11nfromc11  34530  axc11n-16  34542  ax12eq  34545  ax12el  34546  ax12indi  34548  dfac11  37949  intimag  38265  intimasn  38266  frege70  38544  pm11.12  38891  2albi  38894  2exbi  38896  pm11.57  38906  pm11.61  38910  axc5c4c711toc7  38922  axc5c4c711to11  38923  axc11next  38924  pm13.192  38928  ralbidar  38966  rexbidar  38967  hbntal  39086  hbimpg  39087  hbexg  39089  ax6e2nd  39091  hbimpgVD  39454  ax6e2eqVD  39457  ax6e2ndVD  39458  ax6e2ndALT  39480  rexrsb  41490  setrec1lem2  42760  setrec1lem4  42762
  Copyright terms: Public domain W3C validator