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

Theorem alimi 1546
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Aug-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 ax-5 1544 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1535 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  2alimi  1547  al2imi  1548  alrimih  1552  exbi  1568  19.26  1580  19.29  1583  19.25  1590  19.33  1594  equid  1644  alcomiw  1678  hbn1fw  1679  hba1w  1681  hbalw  1683  ax11dgen  1696  hbal  1710  ax5o  1717  hba1  1719  hbimd  1721  dvelimhw  1735  cbv3hv  1737  nfimd  1761  19.21t  1790  dvelimv  1879  ax10  1884  equvini  1927  stdpc4  1964  ax16i  1986  sbco3  2028  sb9i  2034  sbal1  2065  hba1-o  2088  aecom-o  2090  ax11  2094  hbequid  2099  ax67  2104  ax67to6  2106  ax67to7  2107  ax467  2108  ax467to6  2110  ax467to7  2111  equidqe  2112  equid1ALT  2115  ax10from10o  2116  ax10-16  2129  ax11eq  2132  ax11el  2133  ax11indi  2135  mo  2165  eumo0  2167  mo2  2172  2mo  2221  bm1.1  2268  alral  2601  rgen2a  2609  ralimi2  2615  ceqsalt  2810  spcgft  2860  rspct  2877  elabgt  2911  reu6  2954  sbciegft  3021  csbexg  3091  csbnestgf  3129  rabss2  3256  undif4  3511  ralf0  3560  intmin4  3891  dfiin2g  3936  invdisj  4012  trint  4128  axrep2  4133  ax9vsep  4145  axnul  4148  nfnid  4204  axpr  4213  ssrelrel  4787  issref  5056  iotanul  5234  iota4  5237  fv3  5541  zfrep6  5748  ssoprab2  5904  tfrlem5  6396  dfom3  7348  dfac5  7755  dfac2a  7756  dfac2  7757  kmlem1  7776  kmlem13  7788  zorng  8131  brdom3  8153  brdom4  8155  axpowndlem2  8220  axacndlem1  8229  axacndlem2  8230  axacndlem3  8231  axacndlem4  8232  axacnd  8234  ingru  8437  dfnn2  9759  sumeq2w  12165  2ndcdisj2  17183  pjnormssi  22748  ssrmo  23148  disjin  23362  elpotr  24137  dfon2lem8  24146  distel  24160  hbimtg  24163  nninfnub  26461  dfac11  27160  stdpc4-2  27569  pm11.12  27571  2albi  27576  2exim  27577  2exbi  27578  pm11.57  27588  pm11.61  27592  ax4567to6  27604  ax4567to7  27605  ax10ext  27606  pm13.192  27610  ralbidar  27648  rexbidar  27649  rexrsb  27947  hbntal  28319  hbimpg  28320  hbexg  28322  a9e2nd  28324  hbimpgVD  28680  a9e2eqVD  28683  a9e2ndVD  28684  a9e2ndALT  28707  bnj956  28808  bnj1476  28879  bnj1533  28884  bnj1172  29031  bnj1174  29033  bnj1176  29035  bnj1523  29101  a12stdy2-x12  29112  a12study4  29117  ax10lem17ALT  29123  ax10lem18ALT  29124  a12stdy3  29128  a12study  29132  a12study10  29136  a12study10n  29137  a12study11  29138  a12study11n  29139  ax9lem1  29140  ax9lem5  29144  ax9lem7  29146  ax9lem9  29148  ax9lem13  29152  ax9lem17  29156
This theorem was proved from axioms:  ax-mp 8  ax-gen 1533  ax-5 1544
  Copyright terms: Public domain W3C validator