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

Theorem an4s 800
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 798 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  <->  ( ( ph  /\  ps )  /\  ( ch  /\  th )
) )
2 an4s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
31, 2sylbi 188 1  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  an42s  801  anandis  804  anandirs  805  2mo  2340  frminex  4530  trin2  5224  fnun  5518  2elresin  5523  f1co  5615  f1oun  5661  f1oco  5665  f1mpt  5974  poxp  6425  soxp  6426  tfrlem2  6604  tfrlem5  6608  oeoe  6809  brecop  6964  th3qlem1  6977  ovec  6981  pmss12g  7007  dif1enOLD  7307  dif1en  7308  fiin  7393  tcmin  7644  harval2  7848  genpv  8840  genpdm  8843  genpnnp  8846  genpcd  8847  genpnmax  8848  addcmpblnr  8911  mulcmpblnr  8913  addsrpr  8914  mulsrpr  8915  ltsrpr  8916  addclsr  8922  mulclsr  8923  addasssr  8927  mulasssr  8929  distrsr  8930  mulgt0sr  8944  addresr  8977  mulresr  8978  axaddf  8984  axmulf  8985  axaddass  8995  axmulass  8996  axdistr  8997  mulgt0  9117  mul4  9199  add4  9245  2addsub  9283  addsubeq4  9284  sub4  9310  muladd  9430  mulsub  9440  mulge0  9509  mulge0OLD  9510  add20i  9534  mulge0i  9538  mulne0  9628  divmuldiv  9678  rec11i  9719  ltmul12a  9830  zmulcl  10288  uz2mulcl  10517  qaddcl  10554  qmulcl  10556  qreccl  10558  rpaddcl  10596  xmulgt0  10826  xmulge0  10827  ixxin  10897  ge0addcl  10973  ge0xaddcl  10975  fzm1  11090  serge0  11340  expge1  11380  sqrmo  12020  rexanuz  12112  amgm2  12136  mulcn2  12352  dvds2ln  12843  divalglem6  12881  divalglem8  12883  opoe  13148  omoe  13149  opeo  13150  omeo  13151  pc2dvds  13215  catpropd  13898  spwmo  14621  gimco  15018  efgrelexlemb  15345  tgcl  16997  innei  17152  iunconlem  17451  txbas  17560  txss12  17598  txbasval  17599  tx1stc  17643  fbunfip  17862  tsmsxp  18145  blsscls2  18495  bddnghm  18721  qtopbaslem  18753  iimulcl  18923  icoopnst  18925  iocopnst  18926  iccpnfcnv  18930  pf1ind  19936  mumullem2  20924  fsumvma  20958  lgslem3  21043  pntrsumbnd2  21222  ajmoi  22321  hvadd4  22499  hvsub4  22500  shsel3  22778  shscli  22780  shscom  22782  chj4  22998  5oalem3  23119  5oalem5  23121  5oalem6  23122  hoadd4  23248  adjmo  23296  adjsym  23297  cnvadj  23356  leopmuli  23597  mdslmd1lem2  23790  chirredlem2  23855  chirredi  23858  cdjreui  23896  addltmulALT  23910  reofld  24241  xrge0iifcnv  24280  mulge0b  25152  poseq  25475  wfr3g  25477  wfrlem11  25488  frr3g  25502  frrlem4  25506  frrlem5c  25509  funtransport  25877  btwnconn1lem13  25945  btwnconn1lem14  25946  outsideofeu  25977  outsidele  25978  funray  25986  lineintmo  26003  itg2gt0cn  26167  fzadd2  26343  bndss  26393  isdrngo3  26473  riscer  26502  intidl  26537  psgnghm  27313
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 178  df-an 361
  Copyright terms: Public domain W3C validator