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

Theorem alimi 1549
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 1547 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1538 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  2alimi  1550  al2imi  1551  alrimih  1555  exbi  1571  19.26  1583  19.29  1586  19.25  1593  19.33  1597  equid  1662  alcomiw  1690  hbn1fw  1691  hba1w  1693  hbalw  1695  ax11dgen  1708  hbal  1722  ax5o  1729  hba1  1731  hbimd  1733  dvelimhw  1747  cbv3hv  1749  nfimd  1773  19.21t  1802  dvelimv  1892  ax10  1897  equvini  1940  stdpc4  1977  ax16i  1999  sbco3  2041  sb9i  2047  sbal1  2078  hba1-o  2101  aecom-o  2103  ax11  2107  hbequid  2112  ax67  2117  ax67to6  2119  ax67to7  2120  ax467  2121  ax467to6  2123  ax467to7  2124  equidqe  2125  equid1ALT  2128  ax10from10o  2129  ax10-16  2142  ax11eq  2145  ax11el  2146  ax11indi  2148  mo  2178  eumo0  2180  mo2  2185  2mo  2234  bm1.1  2281  alral  2614  rgen2a  2622  ralimi2  2628  ceqsalt  2823  spcgft  2873  rspct  2890  elabgt  2924  reu6  2967  sbciegft  3034  csbexg  3104  csbnestgf  3142  rabss2  3269  undif4  3524  ralf0  3573  intmin4  3907  dfiin2g  3952  invdisj  4028  trint  4144  axrep2  4149  ax9vsep  4161  axnul  4164  nfnid  4220  axpr  4229  ssrelrel  4803  issref  5072  iotanul  5250  iota4  5253  fv3  5557  zfrep6  5764  ssoprab2  5920  tfrlem5  6412  dfom3  7364  dfac5  7771  dfac2a  7772  dfac2  7773  kmlem1  7792  kmlem13  7804  zorng  8147  brdom3  8169  brdom4  8171  axpowndlem2  8236  axacndlem1  8245  axacndlem2  8246  axacndlem3  8247  axacndlem4  8248  axacnd  8250  ingru  8453  dfnn2  9775  sumeq2w  12181  2ndcdisj2  17199  pjnormssi  22764  ssrmo  23164  disjin  23377  cprodeq2w  24134  elpotr  24208  dfon2lem8  24217  distel  24231  hbimtg  24234  nninfnub  26564  dfac11  27263  stdpc4-2  27672  pm11.12  27674  2albi  27679  2exim  27680  2exbi  27681  pm11.57  27691  pm11.61  27695  ax4567to6  27707  ax4567to7  27708  ax10ext  27709  pm13.192  27713  ralbidar  27751  rexbidar  27752  rexrsb  28050  hbntal  28618  hbimpg  28619  hbexg  28621  a9e2nd  28623  hbimpgVD  28996  a9e2eqVD  28999  a9e2ndVD  29000  a9e2ndALT  29023  bnj956  29124  bnj1476  29195  bnj1533  29200  bnj1172  29347  bnj1174  29349  bnj1176  29351  bnj1523  29417  cbv3hvNEW7  29423  hbalw2AUX7  29424  dvelimhwNEW7  29432  dvelimvNEW7  29439  ax10NEW7  29450  equsalihAUX7  29465  equviniNEW7  29502  ax16iNEW7  29526  stdpc4NEW7  29530  sbco3wAUX7  29561  sbal1NEW7  29587  ax7w1AUX7  29615  ax7w2AUX7  29620  ax7w3AUX7  29621  ax7w6AUX7  29622  ax7w7AUX7  29623  ax7w8AUX7  29624  ax7wnftAUX7  29627  ax7w4AUX7  29628  ax7w5AUX7  29629  ax7w9AUX7  29630  hbalOLD7  29634  sbco3OLD7  29708  sb9iOLD7  29712  a12stdy2-x12  29734  a12study4  29739  ax10lem17ALT  29745  ax10lem18ALT  29746  a12stdy3  29750  a12study  29754  a12study10  29758  a12study10n  29759  a12study11  29760  a12study11n  29761  ax9lem1  29762  ax9lem5  29766  ax9lem7  29768  ax9lem9  29770  ax9lem13  29774  ax9lem17  29778
This theorem was proved from axioms:  ax-mp 8  ax-gen 1536  ax-5 1547
  Copyright terms: Public domain W3C validator