Theorem an4s 596

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 592	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 121	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an42s  597  anandis  600  anandirs  601  trin2  5182  fnun  5492  2elresin  5497  f1co  5613  f1oun  5662  f1oco  5665  f1mpt  5980  poxp  6472  tfrlem7  6593  brecop  6904  th3qlem1  6916  oviec  6920  pmss12g  6961  addcmpblnq  7740  mulcmpblnq  7741  mulpipqqs  7746  mulclnq  7749  mulcanenq  7758  distrnqg  7760  mulcmpblnq0  7817  mulcanenq0ec  7818  mulclnq0  7825  nqnq0a  7827  nqnq0m  7828  distrnq0  7832  genipv  7882  genpelvl  7885  genpelvu  7886  genpml  7890  genpmu  7891  genpcdl  7892  genpcuu  7893  genprndl  7894  genprndu  7895  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  addcmpblnr  8112  ltsrprg  8120  addclsr  8126  mulclsr  8127  addasssrg  8129  addresr  8210  mulresr  8211  axaddass  8245  axmulass  8246  axdistr  8247  mulgt0  8406  mul4  8465  add4  8494  2addsub  8547  addsubeq4  8548  sub4  8578  muladd  8718  mulsub  8735  add20i  8827  mulge0i  8956  mulap0b  8991  divmuldivap  9050  ltmul12a  9198  zmulcl  9707  uz2mulcl  10023  qaddcl  10050  qmulcl  10052  qreccl  10057  rpaddcl  10094  ge0addcl  10399  ge0xaddcl  10401  expge1  11033  rexanuz  11775  amgm2  11906  iooinsup  12067  mulcn2  12102  dvds2ln  12615  opoe  12686  omoe  12687  opeo  12688  omeo  12689  lcmgcd  12880  lcmdvds  12881  pc2dvds  13137  tgcl  15307  innei  15406  txbas  15501  txss12  15509  txbasval  15510  blsscls2  15736  qtopbasss  15764  lgslem3  16343  bj-indind  17180