Theorem an4s 390

Description: Inference rearranging 4 conjuncts in antecedent.

Hypothesis

Ref	Expression
an4s.1	⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)

Assertion

Ref	Expression
an4s	⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) → τ)

Proof of Theorem an4s

Step	Hyp	Ref	Expression
1		an4 388	. 2 ⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) ↔ ((φ ∧ ψ) ∧ (χ ∧ θ)))
2		an4s.1	. 2 ⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)
3	1, 2	sylbi 174	1 ⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) → τ)

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  anandis 394  anandirs 395  fnun 2730  f1co 2783  f1oun 2815  tfrlem2 2950  tfrlem5 2953  brecop 3242  th3qlem1 3250  oprec 3254  undom 3342  mulclpi 3815  addcmpblnq 3846  mulcmpblnq 3847  addpipq 3848  mulpipq 3849  ordpipq 3850  addclpq 3852  mulclpq 3854  addasspq 3857  mulasspq 3859  distrpqlem 3860  distrpq 3861  ltapq 3870  genpnnp 3902  genpcd 3903  genpnmax 3904  prlem934b 3932  prlem934 3933  addcmpblnr 3975  mulcmpblnr 3977  addsrpr 3978  mulsrpr 3979  ltsrpr 3980  addclsr 3986  mulclsr 3987  addasssr 3991  mulasssr 3993  distrsr 3994  mulgt0sr 4008  addresr 4050  mulresr 4051  axaddcl 4066  axmulcl 4068  axaddass 4072  axmulass 4073  axdistr 4074  add4t 4127  mul4t 4177  divmuldivt 4263  nnleltp1t 4448  nnreclt 4522  creur 4532  creui 4533  zaddclt 4590  zmulclt 4596  zltp1let 4597  qaddclt 4642  qmulclt 4644  hvadd4t 5013  hvsub4t 5014  hlimcaui 5141  pjthu 5241  pjthu2 5242  shscl 5282  shscomt 5284  osumlem2 5531  5oalem3 5546  5oalem5 5548  5oalem6 5549

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org