Theorem an42s 512

Description: Inference rearranging 4 conjuncts in antecedent.

Hypothesis

Ref	Expression
an41r3s.1	⊢ (((φ ⋀ ψ) ⋀ (χ ⋀ θ)) → τ)

Assertion

Ref	Expression
an42s	⊢ (((φ ⋀ χ) ⋀ (θ ⋀ ψ)) → τ)

Proof of Theorem an42s

Step	Hyp	Ref	Expression
1		an42 510	. 2 ⊢ (((φ ⋀ ψ) ⋀ (χ ⋀ θ)) ↔ ((φ ⋀ χ) ⋀ (θ ⋀ ψ)))
2		an41r3s.1	. 2 ⊢ (((φ ⋀ ψ) ⋀ (χ ⋀ θ)) → τ)
3	1, 2	sylbir 201	1 ⊢ (((φ ⋀ χ) ⋀ (θ ⋀ ψ)) → τ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  nnmsucr 4254  ecopopreq 4322  sbthlem9 4470  addcmpblnq 5065  addpipq 5067  mulpipq 5068  addclpq 5071  addasspq 5076  distrpq 5080  recmulpq 5083  ltsopq 5088  ltexpq 5093  mulcmpblnr 5196  addsrpr 5197  mulsrpr 5198  mulclsr 5206  mulasssr 5212  distrsr 5213  ltsosr 5216  axmulopr 5279  axmulass 5291  axdistr 5292  subadd4t 5488  mulsubt 5490  tgclt 7636  hosubadd4t 9747

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain