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

Theorem an42s 800
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 799 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
32ancom2s 777 1  |-  ( ( ( ph  /\  ch )  /\  ( th  /\  ps ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  nnmsucr  6623  ecopoveq  6759  sbthlem9  6979  mulcmpblnr  8696  addsrpr  8697  mulsrpr  8698  mulclsr  8706  mulasssr  8712  distrsr  8713  ltsosr  8716  axmulf  8768  axmulass  8779  axdistr  8780  subadd4  9091  mulsub  9222  mgmidmo  14370  tgcl  16707  pntibndlem2  20740  hosubadd4  22394  sigadd  25061  fdc  25867  isdrngo2  26001  unichnidl  26068  acongtr  26477
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