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

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

Proof of Theorem an42s
StepHypRef Expression
1 an41r3s.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
21an4s 829 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
32ancom2s 805 1  |-  ( ( ( ph  /\  ch )  /\  ( th  /\  ps ) )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 187  df-an 371
This theorem is referenced by:  nnmsucr  7313  ecopoveq  7451  sbthlem9  7675  mulclsr  9493  mulasssr  9499  distrsr  9500  ltsosr  9503  axmulf  9555  axmulass  9566  axdistr  9567  subadd4  9901  mulsub  10042  mgmidmo  16212  tgcl  19765  bwth  20205  pntibndlem2  24159  hosubadd4  27159  fdc  31533  isdrngo2  31656  unichnidl  31723  acongtr  35290
  Copyright terms: Public domain W3C validator