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  2221  frminex  4373  trin2  5066  fnun  5350  2elresin  5355  f1co  5446  f1oun  5492  f1oco  5496  f1mpt  5785  poxp  6227  soxp  6228  tfrlem2  6392  tfrlem5  6396  oeoe  6597  brecop  6751  th3qlem1  6764  ovec  6768  pmss12g  6794  dif1enOLD  7090  dif1en  7091  fiin  7175  tcmin  7426  harval2  7630  genpv  8623  genpdm  8626  genpnnp  8629  genpcd  8630  genpnmax  8631  addcmpblnr  8694  mulcmpblnr  8696  addsrpr  8697  mulsrpr  8698  ltsrpr  8699  addclsr  8705  mulclsr  8706  addasssr  8710  mulasssr  8712  distrsr  8713  mulgt0sr  8727  addresr  8760  mulresr  8761  axaddf  8767  axmulf  8768  axaddass  8778  axmulass  8779  axdistr  8780  mulgt0  8900  mul4  8981  add4  9027  2addsub  9065  addsubeq4  9066  sub4  9092  muladd  9212  mulsub  9222  mulge0  9291  mulge0OLD  9292  add20i  9316  mulge0i  9320  mulne0  9410  divmuldiv  9460  rec11i  9501  ltmul12a  9612  zmulcl  10066  uz2mulcl  10295  qaddcl  10332  qmulcl  10334  qreccl  10336  rpaddcl  10374  xmulgt0  10603  xmulge0  10604  ixxin  10673  ge0addcl  10748  ge0xaddcl  10750  fzm1  10862  serge0  11100  expge1  11139  sqrmo  11737  rexanuz  11829  amgm2  11853  mulcn2  12069  dvds2ln  12559  divalglem6  12597  divalglem8  12599  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pc2dvds  12931  catpropd  13612  spwmo  14335  gimco  14732  efgrelexlemb  15059  tgcl  16707  innei  16862  iunconlem  17153  txbas  17262  txss12  17300  txbasval  17301  tx1stc  17344  fbunfip  17564  tsmsxp  17837  blsscls2  18050  bddnghm  18235  qtopbaslem  18267  iimulcl  18435  icoopnst  18437  iocopnst  18438  iccpnfcnv  18442  pf1ind  19438  mumullem2  20418  fsumvma  20452  lgslem3  20537  pntrsumbnd2  20716  ajmoi  21437  hvadd4  21615  hvsub4  21616  shsel3  21894  shscli  21896  shscom  21898  chj4  22114  5oalem3  22235  5oalem5  22237  5oalem6  22238  hoadd4  22364  adjmo  22412  adjsym  22413  cnvadj  22472  leopmuli  22713  mdslmd1lem2  22906  chirredlem2  22971  chirredi  22974  cdjreui  23012  addltmulALT  23026  xrge0iifcnv  23315  mulge0b  24086  poseq  24253  wfr3g  24255  wfrlem11  24266  frr3g  24280  frrlem4  24284  frrlem5c  24287  funtransport  24654  btwnconn1lem13  24722  btwnconn1lem14  24723  outsideofeu  24754  outsidele  24755  funray  24763  lineintmo  24780  rzrlzreq  25336  intcont  25543  lvsovso  25626  fzadd2  26444  bndss  26510  isdrngo3  26590  riscer  26619  intidl  26654  psgnghm  27437
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