Theorem an42s 673

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

Step	Hyp	Ref	Expression
1		an41r3s.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
2	1	an4s 672	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)
3	2	ancom2s 662	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  nnmsucr  8607  ecopoveq  8812  sbthlem9  9079  mulclsr  11064  mulasssr  11070  distrsr  11071  ltsosr  11074  axmulf  11126  axmulass  11137  axdistr  11138  subadd4  11497  mulsub  11652  mgmidmo  18713  isdrng3lem2  20852  tgcl  23126  bwth  23567  pntibndlem2  27755  hosubadd4  32166  pibt2  38063  lindsadd  38264  fdc  38396  isdrngo2  38609  unichnidl  38682  acongtr  43705