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

Theorem alimi 1618
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 1617 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1605 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1379
This theorem was proved from axioms:  ax-mp 5  ax-gen 1603  ax-4 1616
This theorem is referenced by:  2alimi  1619  alrimih  1627  aleximiOLD  1644  ala1  1645  19.38  1647  19.26  1665  19.33  1680  alcomiw  1795  hba1w  1798  hbalw  1800  hbal  1828  axc4  1844  cbv3hv  1940  axc16i  2048  2stdpc4  2079  hba1-o  2212  aecom-o  2214  ax12  2218  hbequid  2223  axc711  2228  axc711toc7  2230  axc711to11  2231  axc5c711  2232  axc5c711toc7  2234  axc5c711to11  2235  equidqe  2236  equid1ALT  2239  axc11nfromc11  2240  axc11n-16  2252  ax12eq  2255  ax12el  2256  ax12indi  2258  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  eumo0OLD  2301  mo2OLD  2318  bm1.1OLD  2425  eqeq1d  2443  ralimi2  2831  rgen2a  2868  rgen2aOLD  2869  ceqsalt  3116  spcgft  3170  rspct  3187  elabgt  3227  reu6  3272  sbciegft  3342  csbeq2  3421  rabss2  3565  csbnestgf  3822  undif4  3865  ralf0  3917  intmin4  4297  dfiin2g  4344  invdisj  4422  trint  4541  axrep2  4546  ax6vsep  4558  axnul  4561  csbexg  4565  csbexgOLD  4567  nfnid  4662  axpr  4671  ssrelrel  5089  issref  5366  iotanul  5552  iota4  5555  fv3  5865  zfrep6  6749  dfom3  8062  dfac5  8507  dfac2a  8508  dfac2  8509  kmlem1  8528  kmlem13  8540  zorng  8882  brdom3  8904  brdom4  8906  axpowndlem2  8971  axpowndlem2OLD  8972  axregnd  8979  axacndlem1  8983  axacndlem2  8984  axacndlem3  8985  axacndlem4  8986  axacnd  8988  ingru  9191  dfnn2  10550  2ndcdisj2  19824  pjnormssi  26952  ssrmo  27258  disjin  27311  prodeq2w  29012  elpotr  29181  dfon2lem8  29190  distel  29204  hbimtg  29207  wl-aleq  29956  wl-lem-nexmo  29984  nninfnub  30212  mpt2bi123f  30539  mptbi12f  30543  dfac11  30976  pm11.12  31227  2albi  31230  2exbi  31232  pm11.57  31242  pm11.61  31246  axc5c4c711toc7  31258  axc5c4c711to11  31259  axc11next  31260  pm13.192  31264  ralbidar  31301  rexbidar  31302  rexrsb  32008  hbntal  33034  hbimpg  33035  hbexg  33037  ax6e2nd  33039  hbimpgVD  33412  ax6e2eqVD  33415  ax6e2ndVD  33416  ax6e2ndALT  33438  bnj956  33542  bnj1476  33612  bnj1533  33617  bnj1172  33764  bnj1174  33766  bnj1176  33768  bnj1523  33834  bj-gl4lem  33897  bj-alanim  33918  bj-2albi  33919  bj-2exbi  33920  bj-alrimhi  33927  bj-hbext  33978  bj-nfalt  33979  bj-nfext  33980  bj-cbv3tb  33985  bj-nfs1t2  33989  bj-stdpc4v  34046  bj-2stdpc4v  34047  bj-axrep2  34087  bj-hbaeb2  34103  bj-equsal1  34109  bj-equsal2  34110  2stdpc5  34114  bj-eumo0  34126  bj-ceqsalt0  34161  bj-ceqsalt1  34162
  Copyright terms: Public domain W3C validator