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  6427  mulcanenq0ec  6428  mulclnq0  6435  nqnq0a  6437  nqnq0m  6438  distrnq0  6442  genipv  6492  genpelvl  6495  genpelvu  6496  genpml  6500  genpmu  6501  genpcdl  6502  genpcuu  6503  genprndl  6504  genprndu  6505  distrlem1prl  6558  distrlem1pru  6559  ltsopr  6570  addcmpblnr  6667  ltsrprg  6675  addclsr  6681  mulclsr  6682  addasssrg  6684  addresr  6734  mulresr  6735  axaddass  6756  axmulass  6757  axdistr  6758  mulgt0  6890  mul4  6942  add4  6969  2addsub  7022  addsubeq4  7023  sub4  7052  muladd  7177  mulsub  7194  add20i  7279  mulge0i  7404  mulap0b  7418  divmuldivap  7470  ltmul12a  7607  zmulcl  8073  uz2mulcl  8321  qaddcl  8346  qmulcl  8348  qreccl  8351  rpaddcl  8381  ge0addcl  8620  expge1  8946  bj-indind  9391