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

Theorem an42s 660
 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 659 . 2 (((𝜑𝜒) ∧ (𝜓𝜃)) → 𝜏)
32ancom2s 649 1 (((𝜑𝜒) ∧ (𝜃𝜓)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  nnmsucr  8237  ecopoveq  8384  sbthlem9  8622  mulclsr  10498  mulasssr  10504  distrsr  10505  ltsosr  10508  axmulf  10560  axmulass  10571  axdistr  10572  subadd4  10922  mulsub  11075  mgmidmo  17865  tgcl  21584  bwth  22025  pntibndlem2  26185  hosubadd4  29607  pibt2  34853  lindsadd  35069  fdc  35202  isdrngo2  35415  unichnidl  35488  acongtr  39962
 Copyright terms: Public domain W3C validator