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

Theorem an42s 827
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
Hypothesis
Ref Expression
an41r3s.1
Assertion
Ref Expression
an42s

Proof of Theorem an42s
StepHypRef Expression
1 an41r3s.1 . . 3
21an4s 826 . 2
32ancom2s 802 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  nnmsucr  7293  ecopoveq  7431  sbthlem9  7655  mulclsr  9482  mulasssr  9488  distrsr  9489  ltsosr  9492  axmulf  9544  axmulass  9555  axdistr  9556  subadd4  9886  mulsub  10024  mgmidmo  15886  tgcl  19471  bwth  19910  pntibndlem2  23776  hosubadd4  26733  fdc  30238  isdrngo2  30361  unichnidl  30428  acongtr  30916
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 185  df-an 371
  Copyright terms: Public domain W3C validator