Theorem an42s 593

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnmsucr  6655  ecopoveq  6798  enqdc  7580  addcmpblnq  7586  addpipqqslem  7588  addpipqqs  7589  addclnq  7594  addcomnqg  7600  distrnqg  7606  recexnq  7609  ltdcnq  7616  ltexnqq  7627  enq0enq  7650  enq0sym  7651  enq0breq  7655  addclnq0  7670  distrnq0  7678  mulclsr  7973  axmulass  8092  axdistr  8093  subadd4  8422  mulsub  8579  mgmidmo  13454  tgcl  14787