Theorem an42s 674

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 673	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)
3	2	ancom2s 663	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  nnmsucr  8613  ecopoveq  8818  sbthlem9  9093  mulclsr  11093  mulasssr  11099  distrsr  11100  ltsosr  11103  axmulf  11155  axmulass  11166  axdistr  11167  subadd4  11526  mulsub  11681  mgmidmo  18752  isdrng3lem2  20915  tgcl  23194  bwth  23635  pntibndlem2  27827  hosubadd4  32295  pibt2  38171  lindsadd  38367  fdc  38495  isdrngo2  38708  unichnidl  38781  acongtr  43819