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

Theorem alimi 1609
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 1608 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1598 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1372
This theorem was proved from axioms:  ax-mp 5  ax-gen 1596  ax-4 1607
This theorem is referenced by:  2alimi  1610  al2imi  1611  alrimih  1617  aleximiOLD  1633  19.38  1634  19.26  1652  19.33  1667  alcomiw  1755  hbn1fw  1756  hba1w  1758  hbalw  1760  ax12dgen  1774  hbal  1788  axc4  1804  cbv3hv  1898  axc16i  2030  stdpc4  2060  2stdpc4  2061  sbco3OLD  2131  sb9iOLD  2144  sbal1OLD  2187  hba1-o  2214  aecom-o  2216  ax12  2220  hbequid  2225  axc711  2230  axc711toc7  2232  axc711to11  2233  axc5c711  2234  axc5c711toc7  2236  axc5c711to11  2237  equidqe  2238  equid1ALT  2241  axc11nfromc11  2242  axc11n-16  2254  ax12eq  2257  ax12el  2258  ax12indi  2260  mo2v  2275  mo2vOLD  2276  mo2vOLDOLD  2277  eumo0OLD  2306  moOLD  2320  mo2OLD  2329  2moOLDOLD  2377  bm1.1OLD  2444  eqeq1d  2462  alral  2822  ralimi2  2847  rgen2a  2884  rgen2aOLD  2885  ceqsalt  3129  spcgft  3183  rspct  3200  elabgt  3240  reu6  3285  sbciegft  3355  csbeq2  3432  rabss2  3576  csbnestgf  3833  undif4  3876  ralf0  3927  intmin4  4304  dfiin2g  4351  invdisj  4429  trint  4548  axrep2  4553  ax6vsep  4565  axnul  4568  csbexg  4572  csbexgOLD  4574  nfnid  4669  axpr  4678  ssrelrel  5094  issref  5371  iotanul  5557  iota4  5560  fv3  5870  zfrep6  6742  dfom3  8053  dfac5  8498  dfac2a  8499  dfac2  8500  kmlem1  8519  kmlem13  8531  zorng  8873  brdom3  8895  brdom4  8897  axpowndlem2  8962  axpowndlem2OLD  8963  axregnd  8970  axacndlem1  8974  axacndlem2  8975  axacndlem3  8976  axacndlem4  8977  axacnd  8979  ingru  9182  dfnn2  10538  2ndcdisj2  19717  pjnormssi  26613  ssrmo  26919  disjin  26969  prodeq2w  28471  elpotr  28640  dfon2lem8  28649  distel  28663  hbimtg  28666  wl-aleq  29415  wl-lem-nexmo  29443  nninfnub  29698  mpt2bi123f  30026  mptbi12f  30030  dfac11  30465  pm11.12  30677  2albi  30680  2exbi  30682  pm11.57  30692  pm11.61  30696  axc5c4c711toc7  30708  axc5c4c711to11  30709  axc11next  30710  pm13.192  30714  ralbidar  30751  rexbidar  30752  rexrsb  31460  hbntal  32281  hbimpg  32282  hbexg  32284  ax6e2nd  32286  hbimpgVD  32659  ax6e2eqVD  32662  ax6e2ndVD  32663  ax6e2ndALT  32685  bnj956  32789  bnj1476  32859  bnj1533  32864  bnj1172  33011  bnj1174  33013  bnj1176  33015  bnj1523  33081  bj-ala1BIS  33136  bj-gl4lem  33140  bj-ala1  33161  bj-alanim  33166  bj-2albi  33167  bj-2exbi  33168  bj-alrimhi  33176  bj-hbext  33221  bj-nfalt  33222  bj-nfext  33223  bj-cbv3tb  33228  bj-nfs1t2  33232  bj-stdpc4v  33290  bj-2stdpc4v  33291  bj-axrep2  33331  bj-hbaeb2  33347  bj-equsal1  33353  bj-equsal2  33354  2stdpc5  33358  bj-eumo0  33370  bj-ceqsalt0  33405  bj-ceqsalt1  33406  frege58b  36767
  Copyright terms: Public domain W3C validator