Theorem an42s 589

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 588	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)
3	2	ancom2s 566	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  6546  ecopoveq  6689  enqdc  7428  addcmpblnq  7434  addpipqqslem  7436  addpipqqs  7437  addclnq  7442  addcomnqg  7448  distrnqg  7454  recexnq  7457  ltdcnq  7464  ltexnqq  7475  enq0enq  7498  enq0sym  7499  enq0breq  7503  addclnq0  7518  distrnq0  7526  mulclsr  7821  axmulass  7940  axdistr  7941  subadd4  8270  mulsub  8427  mgmidmo  13015  tgcl  14300