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

Theorem alimi 1569
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 1567 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1558 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550
This theorem is referenced by:  2alimi  1570  al2imi  1571  alrimih  1575  exbi  1592  19.26  1604  19.29  1607  19.25  1614  19.33  1618  equidOLD  1690  alcomiw  1719  hbn1fw  1720  hbn1fwOLD  1721  hba1w  1723  hbalw  1725  ax11dgen  1738  hbal  1752  ax5o  1766  hba1OLD  1806  19.38  1813  nfimdOLD  1829  hbimdOLD  1836  dvelimhwOLD  1878  cbv3hv  1879  cbv3hvOLD  1880  19.21tOLD  1887  dvelimvOLD  2029  ax10OLD  2033  ax16i  2052  equvini  2084  equviniOLD  2085  stdpc4  2092  sbco3  2165  sb9i  2172  sbal1  2205  hba1-o  2228  aecom-o  2230  ax11  2234  hbequid  2239  ax67  2244  ax67to6  2246  ax67to7  2247  ax467  2248  ax467to6  2250  ax467to7  2251  equidqe  2252  equid1ALT  2255  ax10from10o  2256  ax10-16  2269  ax11eq  2272  ax11el  2273  ax11indi  2275  mo  2305  eumo0  2307  mo2  2312  2mo  2361  bm1.1  2423  alral  2766  rgen2a  2774  ralimi2  2780  ceqsalt  2980  spcgft  3030  rspct  3047  elabgt  3081  reu6  3125  sbciegft  3193  csbexg  3263  csbnestgf  3301  rabss2  3428  undif4  3686  ralf0  3736  intmin4  4081  dfiin2g  4126  invdisj  4203  trint  4319  axrep2  4324  ax9vsep  4336  axnul  4339  nfnid  4395  axpr  4404  ssrelrel  4978  issref  5249  iotanul  5435  iota4  5438  fv3  5746  zfrep6  5970  ssoprab2  6132  tfrlem5  6643  dfom3  7604  dfac5  8011  dfac2a  8012  dfac2  8013  kmlem1  8032  kmlem13  8044  zorng  8386  brdom3  8408  brdom4  8410  axpowndlem2  8475  axacndlem1  8484  axacndlem2  8485  axacndlem3  8486  axacndlem4  8487  axacnd  8489  ingru  8692  dfnn2  10015  sumeq2w  12488  2ndcdisj2  17522  pjnormssi  23673  ssrmo  23983  disjin  24029  prodeq2w  25240  elpotr  25410  dfon2lem8  25419  distel  25433  hbimtg  25436  wl-aleq  26237  nninfnub  26457  dfac11  27139  stdpc4-2  27548  pm11.12  27550  2albi  27555  2exim  27556  2exbi  27557  pm11.57  27567  pm11.61  27571  ax4567to6  27583  ax4567to7  27584  ax10ext  27585  pm13.192  27589  ralbidar  27626  rexbidar  27627  rexrsb  27925  hbntal  28642  hbimpg  28643  hbexg  28645  a9e2nd  28647  hbimpgVD  29018  a9e2eqVD  29021  a9e2ndVD  29022  a9e2ndALT  29044  bnj956  29149  bnj1476  29220  bnj1533  29225  bnj1172  29372  bnj1174  29374  bnj1176  29376  bnj1523  29442  cbv3hvNEW7  29448  hbalw2AUX7  29449  dvelimhwNEW7  29457  dvelimvNEW7  29464  ax10NEW7  29475  equsalihAUX7  29490  equviniNEW7  29529  ax16iNEW7  29553  stdpc4NEW7  29557  sbco3wAUX7  29589  sb8iwAUX7  29591  sbal1NEW7  29617  ax7w3AUX7  29653  ax7w6AUX7  29654  ax7w7AUX7  29655  ax7w8AUX7  29656  ax7wnftAUX7  29659  ax7w4AUX7  29660  ax7w5AUX7  29661  ax7w9AUX7  29662  ax7w10AUX7  29664  ax7w11AUX7  29665  ax7w18AUX7  29679  hbalOLD7  29682  sbco3OLD7  29756  sb9iOLD7  29760
This theorem was proved from axioms:  ax-mp 8  ax-gen 1556  ax-5 1567
  Copyright terms: Public domain W3C validator