Theorem an42s 584

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnmsucr  6465  ecopoveq  6605  enqdc  7312  addcmpblnq  7318  addpipqqslem  7320  addpipqqs  7321  addclnq  7326  addcomnqg  7332  distrnqg  7338  recexnq  7341  ltdcnq  7348  ltexnqq  7359  enq0enq  7382  enq0sym  7383  enq0breq  7387  addclnq0  7402  distrnq0  7410  mulclsr  7705  axmulass  7824  axdistr  7825  subadd4  8152  mulsub  8309  mgmidmo  12615  tgcl  12819