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  6761  ecopoveq  6904  enqdc  7728  addcmpblnq  7734  addpipqqslem  7736  addpipqqs  7737  addclnq  7742  addcomnqg  7748  distrnqg  7754  recexnq  7757  ltdcnq  7764  ltexnqq  7775  enq0enq  7798  enq0sym  7799  enq0breq  7803  addclnq0  7818  distrnq0  7826  mulclsr  8121  axmulass  8240  axdistr  8241  subadd4  8570  mulsub  8728  mgmidmo  13692  tgcl  15165