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

Theorem alimi 1634
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 1633 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1621 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1393
This theorem was proved from axioms:  ax-mp 5  ax-gen 1619  ax-4 1632
This theorem is referenced by:  2alimi  1635  alrimih  1643  aleximiOLD  1660  ala1  1661  19.38  1663  19.26  1681  19.33  1696  alcomiw  1812  hba1w  1815  hbalw  1817  hbal  1845  axc4  1861  cbv3hv  1957  axc16i  2065  2stdpc4  2096  hba1-o  2229  aecom-o  2231  ax12  2235  hbequid  2240  axc711  2245  axc711toc7  2247  axc711to11  2248  axc5c711  2249  axc5c711toc7  2251  axc5c711to11  2252  equidqe  2253  equid1ALT  2256  axc11nfromc11  2257  axc11n-16  2269  ax12eq  2272  ax12el  2273  ax12indi  2275  mo2v  2290  mo2vOLD  2291  mo2vOLDOLD  2292  eumo0OLD  2318  mo2OLD  2335  bm1.1OLD  2441  eqeq1d  2459  ralimi2  2847  rgen2a  2884  rgen2aOLD  2885  ceqsalt  3132  spcgft  3186  rspct  3203  elabgt  3243  reu6  3288  sbciegft  3358  csbeq2  3434  rabss2  3579  csbnestgf  3847  undif4  3886  ralf0  3939  intmin4  4318  dfiin2g  4365  invdisj  4445  trint  4565  axrep2  4570  ax6vsep  4582  axnul  4585  csbexg  4589  csbexgOLD  4591  nfnid  4685  axpr  4694  ssrelrel  5112  issref  5390  iotanul  5572  iota4  5575  fv3  5885  zfrep6  6767  dfom3  8081  dfac5  8526  dfac2a  8527  dfac2  8528  kmlem1  8547  kmlem13  8559  zorng  8901  brdom3  8923  brdom4  8925  axpowndlem2  8990  axpowndlem2OLD  8991  axregnd  8998  axacndlem1  9002  axacndlem2  9003  axacndlem3  9004  axacndlem4  9005  axacnd  9007  ingru  9210  dfnn2  10569  prodeq2w  13731  2ndcdisj2  20084  pjnormssi  27214  ssrmo  27520  disjin  27586  elpotr  29430  dfon2lem8  29439  distel  29453  hbimtg  29456  wl-aleq  30193  wl-lem-nexmo  30221  nninfnub  30449  mpt2bi123f  30776  mptbi12f  30780  dfac11  31212  pm11.12  31484  2albi  31487  2exbi  31489  pm11.57  31499  pm11.61  31503  axc5c4c711toc7  31515  axc5c4c711to11  31516  axc11next  31517  pm13.192  31521  ralbidar  31558  rexbidar  31559  rexrsb  32377  hbntal  33469  hbimpg  33470  hbexg  33472  ax6e2nd  33474  hbimpgVD  33847  ax6e2eqVD  33850  ax6e2ndVD  33851  ax6e2ndALT  33873  bnj956  33978  bnj1476  34048  bnj1533  34053  bnj1172  34200  bnj1174  34202  bnj1176  34204  bnj1523  34270  bj-gl4lem  34326  bj-alanim  34347  bj-2albi  34348  bj-2exbi  34349  bj-alrimhi  34356  bj-hbext  34407  bj-nfalt  34408  bj-nfext  34409  bj-cbv3tb  34414  bj-nfs1t2  34418  bj-stdpc4v  34477  bj-2stdpc4v  34478  bj-axrep2  34518  bj-hbaeb2  34534  bj-equsal1  34540  bj-equsal2  34541  2stdpc5  34545  bj-eumo0  34557  bj-ceqsalt0  34592  bj-ceqsalt1  34593  intimag  37930  intimasn  37931  trclfvcotr  37969
  Copyright terms: Public domain W3C validator