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

Theorem an4s 799
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 797 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ( ph  /\  ps )  /\  ( ch  /\  th )
) )
2 an4s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
31, 2sylbi 187 1  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  an42s  800  anandis  803  anandirs  804  2mo  2287  frminex  4455  trin2  5148  fnun  5432  2elresin  5437  f1co  5529  f1oun  5575  f1oco  5579  f1mpt  5872  poxp  6314  soxp  6315  tfrlem2  6479  tfrlem5  6483  oeoe  6684  brecop  6839  th3qlem1  6852  ovec  6856  pmss12g  6882  dif1enOLD  7180  dif1en  7181  fiin  7265  tcmin  7516  harval2  7720  genpv  8713  genpdm  8716  genpnnp  8719  genpcd  8720  genpnmax  8721  addcmpblnr  8784  mulcmpblnr  8786  addsrpr  8787  mulsrpr  8788  ltsrpr  8789  addclsr  8795  mulclsr  8796  addasssr  8800  mulasssr  8802  distrsr  8803  mulgt0sr  8817  addresr  8850  mulresr  8851  axaddf  8857  axmulf  8858  axaddass  8868  axmulass  8869  axdistr  8870  mulgt0  8990  mul4  9071  add4  9117  2addsub  9155  addsubeq4  9156  sub4  9182  muladd  9302  mulsub  9312  mulge0  9381  mulge0OLD  9382  add20i  9406  mulge0i  9410  mulne0  9500  divmuldiv  9550  rec11i  9591  ltmul12a  9702  zmulcl  10158  uz2mulcl  10387  qaddcl  10424  qmulcl  10426  qreccl  10428  rpaddcl  10466  xmulgt0  10695  xmulge0  10696  ixxin  10765  ge0addcl  10840  ge0xaddcl  10842  fzm1  10954  serge0  11192  expge1  11232  sqrmo  11833  rexanuz  11925  amgm2  11949  mulcn2  12165  dvds2ln  12656  divalglem6  12694  divalglem8  12696  opoe  12961  omoe  12962  opeo  12963  omeo  12964  pc2dvds  13028  catpropd  13711  spwmo  14434  gimco  14831  efgrelexlemb  15158  tgcl  16813  innei  16968  iunconlem  17259  txbas  17368  txss12  17406  txbasval  17407  tx1stc  17450  fbunfip  17666  tsmsxp  17939  blsscls2  18152  bddnghm  18337  qtopbaslem  18369  iimulcl  18539  icoopnst  18541  iocopnst  18542  iccpnfcnv  18546  pf1ind  19542  mumullem2  20530  fsumvma  20564  lgslem3  20649  pntrsumbnd2  20828  ajmoi  21551  hvadd4  21729  hvsub4  21730  shsel3  22008  shscli  22010  shscom  22012  chj4  22228  5oalem3  22349  5oalem5  22351  5oalem6  22352  hoadd4  22478  adjmo  22526  adjsym  22527  cnvadj  22586  leopmuli  22827  mdslmd1lem2  23020  chirredlem2  23085  chirredi  23088  cdjreui  23126  addltmulALT  23140  xrge0iifcnv  23475  mulge0b  24492  poseq  24811  wfr3g  24813  wfrlem11  24824  frr3g  24838  frrlem4  24842  frrlem5c  24845  funtransport  25213  btwnconn1lem13  25281  btwnconn1lem14  25282  outsideofeu  25313  outsidele  25314  funray  25322  lineintmo  25339  itg2gt0cn  25495  fzadd2  25768  bndss  25833  isdrngo3  25913  riscer  25942  intidl  25977  psgnghm  26760
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 177  df-an 360
  Copyright terms: Public domain W3C validator