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  4703  fnun  4992  2elresin  4997  f1co  5088  f1oun  5133  f1oco  5136  f1mpt  5397  poxp  5840  tfrlem7  5920  brecop  6183  th3qlem1  6195  oviec  6199  addcmpblnq  6446  mulcmpblnq  6447  mulpipqqs  6452  mulclnq  6455  mulcanenq  6464  distrnqg  6466  mulcmpblnq0  6523  mulcanenq0ec  6524  mulclnq0  6531  nqnq0a  6533  nqnq0m  6534  distrnq0  6538  genipv  6588  genpelvl  6591  genpelvu  6592  genpml  6596  genpmu  6597  genpcdl  6598  genpcuu  6599  genprndl  6600  genprndu  6601  distrlem1prl  6661  distrlem1pru  6662  ltsopr  6675  addcmpblnr  6805  ltsrprg  6813  addclsr  6819  mulclsr  6820  addasssrg  6822  addresr  6894  mulresr  6895  axaddass  6927  axmulass  6928  axdistr  6929  mulgt0  7073  mul4  7125  add4  7152  2addsub  7205  addsubeq4  7206  sub4  7235  muladd  7360  mulsub  7377  add20i  7462  mulge0i  7587  mulap0b  7612  divmuldivap  7664  ltmul12a  7802  zmulcl  8269  uz2mulcl  8517  qaddcl  8542  qmulcl  8544  qreccl  8547  rpaddcl  8577  ge0addcl  8817  serige0  9130  expge1  9170  rexanuz  9465  amgm2  9592  mulcn2  9710  bj-indind  9929