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

Theorem alimi 1681
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 1680 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1668 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1436
This theorem was proved from axioms:  ax-mp 5  ax-gen 1666  ax-4 1679
This theorem is referenced by:  2alimi  1682  alrimih  1690  ala1  1706  19.38  1708  19.26  1726  19.33  1740  alcomiw  1862  hba1w  1865  hbalw  1867  hbal  1895  axc4  1912  cbv3hv  2013  axc16i  2120  2stdpc4  2149  mo2v  2273  mo2vOLD  2274  bm1.1OLD  2407  eqeq1d  2425  ralimi2  2816  rgen2a  2853  rgen2aOLD  2854  ceqsalt  3105  spcgft  3159  rspct  3176  elabgt  3216  reu6  3261  sbciegft  3331  csbeq2  3400  rabss2  3545  csbnestgf  3814  undif4  3850  ralf0  3905  intmin4  4283  dfiin2g  4330  invdisj  4410  trint  4531  axrep2  4536  ax6vsep  4548  axnul  4551  axnulOLD  4552  csbexg  4556  nfnid  4648  axpr  4657  ssrelrel  4952  issref  5230  iotanul  5578  iota4  5581  fv3  5892  zfrep6  6773  dfom3  8156  dfac5  8561  dfac2a  8562  dfac2  8563  kmlem1  8582  kmlem13  8594  zorng  8936  brdom3  8958  brdom4  8960  axpowndlem2  9025  axregnd  9031  axacndlem1  9034  axacndlem2  9035  axacndlem3  9036  axacndlem4  9037  axacnd  9039  ingru  9242  dfnn2  10624  trclfvcotr  13067  prodeq2w  13959  2ndcdisj2  20464  pjnormssi  27813  ssrmo  28122  disjin  28192  disjin2  28193  bnj956  29590  bnj1476  29660  bnj1533  29665  bnj1172  29812  bnj1174  29814  bnj1176  29816  bnj1523  29882  elpotr  30428  dfon2lem8  30437  distel  30451  hbimtg  30454  bj-gl4lem  31176  bj-alanim  31197  bj-2albi  31198  bj-2exbi  31199  bj-alrimhi  31206  bj-hbext  31258  bj-nfalt  31259  bj-nfext  31260  bj-cbv3tb  31265  bj-nfs1t2  31269  bj-stdpc4v  31327  bj-2stdpc4v  31328  bj-axrep2  31368  bj-hbaeb2  31384  bj-equsal1  31390  bj-equsal2  31391  2stdpc5  31395  bj-eumo0  31407  bj-ceqsalt0  31446  bj-ceqsalt1  31447  wl-aleq  31826  wl-lem-nexmo  31854  wl-ax12  31871  phpreu  31887  nninfnub  32038  mpt2bi123f  32364  mptbi12f  32368  hba1-o  32432  aecom-o  32434  ax12  32438  hbequid  32443  axc711  32448  axc711toc7  32450  axc711to11  32451  axc5c711  32452  axc5c711toc7  32454  axc5c711to11  32455  equidqe  32456  equid1ALT  32459  axc11nfromc11  32460  axc11n-16  32472  ax12eq  32475  ax12el  32476  ax12indi  32478  dfac11  35884  intimag  36152  intimasn  36153  frege70  36431  pm11.12  36626  2albi  36629  2exbi  36631  pm11.57  36641  pm11.61  36645  axc5c4c711toc7  36657  axc5c4c711to11  36658  axc11next  36659  pm13.192  36663  ralbidar  36700  rexbidar  36701  hbntal  36822  hbimpg  36823  hbexg  36825  ax6e2nd  36827  hbimpgVD  37206  ax6e2eqVD  37209  ax6e2ndVD  37210  ax6e2ndALT  37232  rexrsb  38347
  Copyright terms: Public domain W3C validator