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

Theorem alimi 1605
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)
Hypothesis
Ref Expression
alimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
alimi  |-  ( A. x ph  ->  A. x ps )

Proof of Theorem alimi
StepHypRef Expression
1 alim 1604 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1594 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368
This theorem was proved from axioms:  ax-mp 5  ax-gen 1592  ax-4 1603
This theorem is referenced by:  2alimi  1606  al2imi  1607  alrimih  1613  aleximiOLD  1629  19.38  1630  19.26  1648  19.33  1663  alcomiw  1751  hbn1fw  1752  hba1w  1754  hbalw  1756  ax12dgen  1770  hbal  1784  axc4  1797  cbv3hv  1891  axc16i  2021  stdpc4  2051  2stdpc4  2052  sbco3OLD  2122  sb9iOLD  2135  sbal1OLD  2179  hba1-o  2206  aecom-o  2208  ax12  2212  hbequid  2217  axc711  2222  axc711toc7  2224  axc711to11  2225  axc5c711  2226  axc5c711toc7  2228  axc5c711to11  2229  equidqe  2230  equid1ALT  2233  axc11nfromc11  2234  axc11n-16  2246  ax12eq  2249  ax12el  2250  ax12indi  2252  mo2v  2267  mo2vOLD  2268  mo2vOLDOLD  2269  eumo0OLD  2298  moOLD  2312  mo2OLD  2321  2moOLDOLD  2369  bm1.1OLD  2435  eqeq1d  2453  alral  2805  ralimi2  2808  rgen2a  2892  ceqsalt  3093  spcgft  3147  rspct  3164  elabgt  3202  reu6  3247  sbciegft  3317  csbeq2  3392  rabss2  3535  csbnestgf  3792  undif4  3835  ralf0  3886  intmin4  4257  dfiin2g  4303  invdisj  4381  trint  4500  axrep2  4505  ax6vsep  4517  axnul  4520  csbexg  4524  csbexgOLD  4526  nfnid  4621  axpr  4630  ssrelrel  5040  issref  5311  iotanul  5496  iota4  5499  fv3  5804  zfrep6  6647  dfom3  7956  dfac5  8401  dfac2a  8402  dfac2  8403  kmlem1  8422  kmlem13  8434  zorng  8776  brdom3  8798  brdom4  8800  axpowndlem2  8865  axpowndlem2OLD  8866  axregnd  8873  axacndlem1  8877  axacndlem2  8878  axacndlem3  8879  axacndlem4  8880  axacnd  8882  ingru  9085  dfnn2  10438  2ndcdisj2  19179  pjnormssi  25709  ssrmo  26015  disjin  26065  prodeq2w  27561  elpotr  27730  dfon2lem8  27739  distel  27753  hbimtg  27756  wl-aleq  28504  wl-lem-nexmo  28532  nninfnub  28787  mpt2bi123f  29115  mptbi12f  29119  dfac11  29555  pm11.12  29767  2albi  29770  2exbi  29772  pm11.57  29782  pm11.61  29786  axc5c4c711toc7  29798  axc5c4c711to11  29799  axc11next  29800  pm13.192  29804  ralbidar  29841  rexbidar  29842  rexrsb  30133  hbntal  31564  hbimpg  31565  hbexg  31567  ax6e2nd  31569  hbimpgVD  31942  ax6e2eqVD  31945  ax6e2ndVD  31946  ax6e2ndALT  31968  bnj956  32072  bnj1476  32142  bnj1533  32147  bnj1172  32294  bnj1174  32296  bnj1176  32298  bnj1523  32364  bj-ala1BIS  32428  bj-ala1  32442  bj-alanim  32447  bj-2albi  32448  bj-2exbi  32449  bj-alrimhi  32457  bj-hbext  32502  bj-nfalt  32503  bj-nfext  32504  bj-cbv3tb  32509  bj-nfs1t2  32513  bj-stdpc4v  32571  bj-2stdpc4v  32572  bj-axrep2  32612  bj-equsal1  32634  bj-equsal2  32635  2stdpc5  32639  bj-eumo0  32651  bj-ceqsalt0  32686  bj-ceqsalt1  32687
  Copyright terms: Public domain W3C validator