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

Theorem alimi 1684
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 1683 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
2 alimi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1671 1  |-  ( A. x ph  ->  A. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1442
This theorem was proved from axioms:  ax-mp 5  ax-gen 1669  ax-4 1682
This theorem is referenced by:  2alimi  1685  alrimih  1693  ala1  1710  19.38  1712  19.26  1732  19.33  1747  alcomiw  1880  hba1w  1883  hbalw  1885  hbal  1922  axc4  1938  cbv3hvOLDOLD  2063  axc16i  2156  2stdpc4  2185  mo2v  2306  eqeq1d  2453  ralimi2  2778  rgen2a  2815  rgen2aOLD  2816  ceqsalt  3070  spcgft  3126  rspct  3143  elabgt  3182  reu6  3227  sbciegft  3298  csbeq2  3367  rabss2  3512  csbnestgf  3785  undif4  3821  ralf0  3876  intmin4  4264  dfiin2g  4311  invdisj  4391  trint  4512  axrep2  4517  ax6vsep  4529  axnul  4532  axnulOLD  4533  csbexg  4537  nfnid  4629  axpr  4638  ssrelrel  4935  issref  5213  iotanul  5561  iota4  5564  fv3  5878  zfrep6  6761  dfom3  8152  dfac5  8559  dfac2a  8560  dfac2  8561  kmlem1  8580  kmlem13  8592  zorng  8934  brdom3  8956  brdom4  8958  axpowndlem2  9023  axregnd  9029  axacndlem1  9032  axacndlem2  9033  axacndlem3  9034  axacndlem4  9035  axacnd  9037  ingru  9240  dfnn2  10622  trclfvcotr  13073  prodeq2w  13966  2ndcdisj2  20472  pjnormssi  27821  ssrmo  28130  disjin  28196  disjin2  28197  bnj956  29588  bnj1476  29658  bnj1533  29663  bnj1172  29810  bnj1174  29812  bnj1176  29814  bnj1523  29880  elpotr  30427  dfon2lem8  30436  distel  30450  hbimtg  30453  bj-gl4lem  31178  bj-alanim  31204  bj-2albi  31205  bj-2exbi  31206  bj-alrimhi  31213  bj-ssbbi  31235  bj-ssb1a  31245  bj-ssbequ2  31256  bj-ssbid2ALT  31259  bj-hbext  31304  bj-nfalt  31305  bj-nfext  31306  bj-cbv3tb  31312  bj-nfs1t2  31316  bj-stdpc4v  31366  bj-2stdpc4v  31367  bj-axrep2  31404  bj-hbaeb2  31420  bj-equsal1  31426  bj-equsal2  31427  2stdpc5  31431  bj-eumo0  31443  bj-ceqsalt0  31482  bj-ceqsalt1  31483  wl-aleq  31868  wl-lem-nexmo  31896  wl-ax12  31913  phpreu  31929  nninfnub  32080  mpt2bi123f  32406  mptbi12f  32410  hba1-o  32469  aecom-o  32471  ax12  32475  hbequid  32480  axc711  32485  axc711toc7  32487  axc711to11  32488  axc5c711  32489  axc5c711toc7  32491  axc5c711to11  32492  equidqe  32493  equid1ALT  32496  axc11nfromc11  32497  axc11n-16  32509  ax12eq  32512  ax12el  32513  ax12indi  32515  dfac11  35920  intimag  36248  intimasn  36249  frege70  36529  pm11.12  36724  2albi  36727  2exbi  36729  pm11.57  36739  pm11.61  36743  axc5c4c711toc7  36755  axc5c4c711to11  36756  axc11next  36757  pm13.192  36761  ralbidar  36798  rexbidar  36799  hbntal  36920  hbimpg  36921  hbexg  36923  ax6e2nd  36925  hbimpgVD  37301  ax6e2eqVD  37304  ax6e2ndVD  37305  ax6e2ndALT  37327  rexrsb  38590  falseral0  38986
  Copyright terms: Public domain W3C validator