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

Theorem an42s 802
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 801 . 2  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  th ) )  ->  ta )
32ancom2s 779 1  |-  ( ( ( ph  /\  ch )  /\  ( th  /\  ps ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  nnmsucr  6871  ecopoveq  7008  sbthlem9  7228  mulcmpblnr  8954  addsrpr  8955  mulsrpr  8956  mulclsr  8964  mulasssr  8970  distrsr  8971  ltsosr  8974  axmulf  9026  axmulass  9037  axdistr  9038  subadd4  9350  mulsub  9481  mgmidmo  14698  tgcl  17039  pntibndlem2  21290  hosubadd4  23322  fdc  26463  isdrngo2  26588  unichnidl  26655  acongtr  27057
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 179  df-an 362
  Copyright terms: Public domain W3C validator