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

Theorem an4s 826
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an4s.1
Assertion
Ref Expression
an4s

Proof of Theorem an4s
StepHypRef Expression
1 an4 824 . 2
2 an4s.1 . 2
31, 2sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  an42s  827  anandis  830  anandirs  831  nfeqf  2045  frminex  4864  trin2  5395  fnun  5692  2elresin  5697  f1co  5795  f1oun  5840  f1oco  5843  f1mpt  6169  poxp  6912  soxp  6913  tfrlem7  7071  oeoe  7267  brecop  7423  pmss12g  7465  dif1enOLD  7772  dif1en  7773  fiin  7902  tcmin  8193  harval2  8399  genpv  9398  genpdm  9401  genpnnp  9404  genpcd  9405  genpnmax  9406  addcmpblnr  9467  ltsrpr  9475  addclsr  9481  mulclsr  9482  addasssr  9486  mulasssr  9488  distrsr  9489  mulgt0sr  9503  addresr  9536  mulresr  9537  axaddf  9543  axmulf  9544  axaddass  9554  axmulass  9555  axdistr  9556  mulgt0  9683  mul4  9770  add4  9817  2addsub  9857  addsubeq4  9858  sub4  9887  muladd  10014  mulsub  10024  mulge0  10095  mulge0OLD  10096  add20i  10121  mulge0i  10125  mulne0  10216  divmuldiv  10269  rec11i  10310  ltmul12a  10423  mulge0b  10437  zmulcl  10937  uz2mulcl  11188  qaddcl  11227  qmulcl  11229  qreccl  11231  rpaddcl  11269  xmulgt0  11504  xmulge0  11505  ixxin  11575  ge0addcl  11661  ge0xaddcl  11663  serge0  12161  expge1  12203  sqrmo  13085  rexanuz  13178  amgm2  13202  mulcn2  13418  dvds2ln  14014  divalglem6  14056  divalglem8  14058  opoe  14335  omoe  14336  opeo  14337  omeo  14338  pc2dvds  14402  catpropd  15104  gimco  16316  efgrelexlemb  16768  pf1ind  18391  psgnghm  18616  tgcl  19471  innei  19626  iunconlem  19928  txbas  20068  txss12  20106  txbasval  20107  tx1stc  20151  fbunfip  20370  tsmsxp  20657  blsscls2  21007  bddnghm  21233  qtopbaslem  21265  iimulcl  21437  icoopnst  21439  iocopnst  21440  iccpnfcnv  21444  mumullem2  23454  fsumvma  23488  lgslem3  23573  pntrsumbnd2  23752  ajmoi  25774  hvadd4  25953  hvsub4  25954  shsel3  26233  shscli  26235  shscom  26237  chj4  26453  5oalem3  26574  5oalem5  26576  5oalem6  26577  hoadd4  26703  adjmo  26751  adjsym  26752  cnvadj  26811  leopmuli  27052  mdslmd1lem2  27245  chirredlem2  27310  chirredi  27313  cdjreui  27351  addltmulALT  27365  reofld  27830  xrge0iifcnv  27915  poseq  29333  wfr3g  29342  wfrlem11  29353  frr3g  29386  frrlem4  29390  frrlem5c  29393  funtransport  29681  btwnconn1lem13  29749  btwnconn1lem14  29750  outsideofeu  29781  outsidele  29782  funray  29790  lineintmo  29807  heicant  30049  itg2gt0cn  30070  fzadd2  30234  bndss  30282  isdrngo3  30362  riscer  30391  intidl  30426  unxpwdom3  31041  lcmcllem  31202  lcmgcd  31213  lcmdvds  31214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator