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

Theorem alimi 1654
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 1653 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1641 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1403
This theorem was proved from axioms:  ax-mp 5  ax-gen 1639  ax-4 1652
This theorem is referenced by:  2alimi  1655  alrimih  1663  aleximiOLD  1680  ala1  1681  19.38  1683  19.26  1701  19.33  1716  alcomiw  1835  hba1w  1838  hbalw  1840  hbal  1868  axc4  1884  cbv3hv  1984  axc16i  2090  2stdpc4  2119  mo2v  2245  mo2vOLD  2246  mo2vOLDOLD  2247  bm1.1OLD  2386  eqeq1d  2404  ralimi2  2794  rgen2a  2831  rgen2aOLD  2832  ceqsalt  3082  spcgft  3136  rspct  3153  elabgt  3193  reu6  3238  sbciegft  3308  csbeq2  3377  rabss2  3522  csbnestgf  3790  undif4  3826  ralf0  3880  intmin4  4257  dfiin2g  4304  invdisj  4384  trint  4504  axrep2  4509  ax6vsep  4521  axnul  4524  csbexg  4528  nfnid  4620  axpr  4629  ssrelrel  4924  issref  5201  iotanul  5548  iota4  5551  fv3  5862  zfrep6  6752  dfom3  8097  dfac5  8541  dfac2a  8542  dfac2  8543  kmlem1  8562  kmlem13  8574  zorng  8916  brdom3  8938  brdom4  8940  axpowndlem2  9005  axregnd  9011  axacndlem1  9015  axacndlem2  9016  axacndlem3  9017  axacndlem4  9018  axacnd  9020  ingru  9223  dfnn2  10589  trclfvcotr  12992  prodeq2w  13871  2ndcdisj2  20250  pjnormssi  27500  ssrmo  27808  disjin  27878  disjin2  27879  bnj956  29162  bnj1476  29232  bnj1533  29237  bnj1172  29384  bnj1174  29386  bnj1176  29388  bnj1523  29454  elpotr  30000  dfon2lem8  30009  distel  30023  hbimtg  30026  bj-gl4lem  30747  bj-alanim  30768  bj-2albi  30769  bj-2exbi  30770  bj-alrimhi  30777  bj-hbext  30828  bj-nfalt  30829  bj-nfext  30830  bj-cbv3tb  30835  bj-nfs1t2  30839  bj-stdpc4v  30898  bj-2stdpc4v  30899  bj-axrep2  30939  bj-hbaeb2  30955  bj-equsal1  30961  bj-equsal2  30962  2stdpc5  30966  bj-eumo0  30978  bj-ceqsalt0  31013  bj-ceqsalt1  31014  wl-aleq  31355  wl-lem-nexmo  31383  wl-ax12  31395  nninfnub  31526  mpt2bi123f  31853  mptbi12f  31857  hba1-o  31921  aecom-o  31923  ax12  31927  hbequid  31932  axc711  31937  axc711toc7  31939  axc711to11  31940  axc5c711  31941  axc5c711toc7  31943  axc5c711to11  31944  equidqe  31945  equid1ALT  31948  axc11nfromc11  31949  axc11n-16  31961  ax12eq  31964  ax12el  31965  ax12indi  31967  dfac11  35370  intimag  35635  intimasn  35636  frege70  35914  pm11.12  36128  2albi  36131  2exbi  36133  pm11.57  36143  pm11.61  36147  axc5c4c711toc7  36159  axc5c4c711to11  36160  axc11next  36161  pm13.192  36165  ralbidar  36202  rexbidar  36203  hbntal  36350  hbimpg  36351  hbexg  36353  ax6e2nd  36355  hbimpgVD  36735  ax6e2eqVD  36738  ax6e2ndVD  36739  ax6e2ndALT  36761  rexrsb  37542
  Copyright terms: Public domain W3C validator