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

Theorem an42s 887
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 886 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 861 1 (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  nnmsucr  7750  ecopoveq  7891  sbthlem9  8119  mulclsr  9943  mulasssr  9949  distrsr  9950  ltsosr  9953  axmulf  10005  axmulass  10016  axdistr  10017  subadd4  10363  mulsub  10511  mgmidmo  17306  tgcl  20821  bwth  21261  pntibndlem2  25325  hosubadd4  28801  fdc  33671  isdrngo2  33887  unichnidl  33960  acongtr  37862
  Copyright terms: Public domain W3C validator