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

Theorem an42s 659
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 658 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 648 1 (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  nnmsucr  8621  ecopoveq  8808  sbthlem9  9087  mulclsr  11075  mulasssr  11081  distrsr  11082  ltsosr  11085  axmulf  11137  axmulass  11148  axdistr  11149  subadd4  11500  mulsub  11653  mgmidmo  18575  tgcl  22463  bwth  22905  pntibndlem2  27083  hosubadd4  31054  pibt2  36286  lindsadd  36469  fdc  36601  isdrngo2  36814  unichnidl  36887  acongtr  41702
  Copyright terms: Public domain W3C validator