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

Theorem an4s 801
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an4s.1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Assertion
Ref Expression
an4s  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )

Proof of Theorem an4s
StepHypRef Expression
1 an4 799 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ( ph  /\  ps )  /\  ( ch  /\  th )
) )
2 an4s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
31, 2sylbi 189 1  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  an42s  802  anandis  805  anandirs  806  2mo  2360  frminex  4563  trin2  5258  fnun  5552  2elresin  5557  f1co  5649  f1oun  5695  f1oco  5699  f1mpt  6008  poxp  6459  soxp  6460  tfrlem2  6638  tfrlem5  6642  oeoe  6843  brecop  6998  th3qlem1  7011  ovec  7015  pmss12g  7041  dif1enOLD  7341  dif1en  7342  fiin  7428  tcmin  7681  harval2  7885  genpv  8877  genpdm  8880  genpnnp  8883  genpcd  8884  genpnmax  8885  addcmpblnr  8948  mulcmpblnr  8950  addsrpr  8951  mulsrpr  8952  ltsrpr  8953  addclsr  8959  mulclsr  8960  addasssr  8964  mulasssr  8966  distrsr  8967  mulgt0sr  8981  addresr  9014  mulresr  9015  axaddf  9021  axmulf  9022  axaddass  9032  axmulass  9033  axdistr  9034  mulgt0  9154  mul4  9236  add4  9282  2addsub  9320  addsubeq4  9321  sub4  9347  muladd  9467  mulsub  9477  mulge0  9546  mulge0OLD  9547  add20i  9571  mulge0i  9575  mulne0  9665  divmuldiv  9715  rec11i  9756  ltmul12a  9867  zmulcl  10325  uz2mulcl  10554  qaddcl  10591  qmulcl  10593  qreccl  10595  rpaddcl  10633  xmulgt0  10863  xmulge0  10864  ixxin  10934  ge0addcl  11010  ge0xaddcl  11012  fzm1  11128  serge0  11378  expge1  11418  sqrmo  12058  rexanuz  12150  amgm2  12174  mulcn2  12390  dvds2ln  12881  divalglem6  12919  divalglem8  12921  opoe  13186  omoe  13187  opeo  13188  omeo  13189  pc2dvds  13253  catpropd  13936  spwmo  14659  gimco  15056  efgrelexlemb  15383  tgcl  17035  innei  17190  iunconlem  17491  txbas  17600  txss12  17638  txbasval  17639  tx1stc  17683  fbunfip  17902  tsmsxp  18185  blsscls2  18535  bddnghm  18761  qtopbaslem  18793  iimulcl  18963  icoopnst  18965  iocopnst  18966  iccpnfcnv  18970  pf1ind  19976  mumullem2  20964  fsumvma  20998  lgslem3  21083  pntrsumbnd2  21262  ajmoi  22361  hvadd4  22539  hvsub4  22540  shsel3  22818  shscli  22820  shscom  22822  chj4  23038  5oalem3  23159  5oalem5  23161  5oalem6  23162  hoadd4  23288  adjmo  23336  adjsym  23337  cnvadj  23396  leopmuli  23637  mdslmd1lem2  23830  chirredlem2  23895  chirredi  23898  cdjreui  23936  addltmulALT  23950  reofld  24281  xrge0iifcnv  24320  mulge0b  25192  poseq  25529  wfr3g  25538  wfrlem11  25549  frr3g  25582  frrlem4  25586  frrlem5c  25589  funtransport  25966  btwnconn1lem13  26034  btwnconn1lem14  26035  outsideofeu  26066  outsidele  26067  funray  26075  lineintmo  26092  itg2gt0cn  26261  fzadd2  26446  bndss  26496  isdrngo3  26576  riscer  26605  intidl  26640  psgnghm  27415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator