Theorem an4s 522

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

Hypothesis

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

Assertion

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

Proof of Theorem an4s

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  an42s  523  anandis  526  anandirs  527  trin2  4659  fnun  4948  2elresin  4953  f1co  5044  f1oun  5089  f1oco  5092  f1mpt  5353  poxp  5794  tfrlem7  5874  brecop  6132  th3qlem1  6144  oviec  6148  addcmpblnq  6351  mulcmpblnq  6352  mulpipqqs  6357  mulclnq  6360  mulcanenq  6369  distrnqg  6371  mulcmpblnq0  6426  mulcanenq0ec  6427  mulclnq0  6434  nqnq0a  6436  nqnq0m  6437  distrnq0  6441  genipv  6491  genpelvl  6494  genpelvu  6495  genpml  6499  genpmu  6500  genpcdl  6501  genpcuu  6502  genprndl  6503  genprndu  6504  distrlem1prl  6557  distrlem1pru  6558  ltsopr  6569  addcmpblnr  6647  ltsrprg  6655  addclsr  6661  mulclsr  6662  addasssrg  6664  addresr  6714  mulresr  6715  axaddass  6736  axmulass  6737  axdistr  6738  mulgt0  6870  mul4  6922  add4  6949  2addsub  7002  addsubeq4  7003  sub4  7032  muladd  7157  mulsub  7174  add20i  7259  mulge0i  7384  mulap0b  7398  divmuldivap  7450  ltmul12a  7587  zmulcl  8053  uz2mulcl  8301  qaddcl  8326  qmulcl  8328  qreccl  8331  rpaddcl  8361  ge0addcl  8600  expge1  8926