Theorem an42s 597

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  nnmsucr  6765  ecopoveq  6908  enqdc  7734  addcmpblnq  7740  addpipqqslem  7742  addpipqqs  7743  addclnq  7748  addcomnqg  7754  distrnqg  7760  recexnq  7763  ltdcnq  7770  ltexnqq  7781  enq0enq  7804  enq0sym  7805  enq0breq  7809  addclnq0  7824  distrnq0  7832  mulclsr  8127  axmulass  8246  axdistr  8247  subadd4  8577  mulsub  8735  mgmidmo  13751  tgcl  15290