Theorem an4s 590

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an42s  591  anandis  594  anandirs  595  trin2  5119  fnun  5428  2elresin  5433  f1co  5542  f1oun  5591  f1oco  5594  f1mpt  5894  poxp  6376  tfrlem7  6461  brecop  6770  th3qlem1  6782  oviec  6786  pmss12g  6820  addcmpblnq  7550  mulcmpblnq  7551  mulpipqqs  7556  mulclnq  7559  mulcanenq  7568  distrnqg  7570  mulcmpblnq0  7627  mulcanenq0ec  7628  mulclnq0  7635  nqnq0a  7637  nqnq0m  7638  distrnq0  7642  genipv  7692  genpelvl  7695  genpelvu  7696  genpml  7700  genpmu  7701  genpcdl  7702  genpcuu  7703  genprndl  7704  genprndu  7705  distrlem1prl  7765  distrlem1pru  7766  ltsopr  7779  addcmpblnr  7922  ltsrprg  7930  addclsr  7936  mulclsr  7937  addasssrg  7939  addresr  8020  mulresr  8021  axaddass  8055  axmulass  8056  axdistr  8057  mulgt0  8217  mul4  8274  add4  8303  2addsub  8356  addsubeq4  8357  sub4  8387  muladd  8526  mulsub  8543  add20i  8635  mulge0i  8763  mulap0b  8798  divmuldivap  8855  ltmul12a  9003  zmulcl  9496  uz2mulcl  9799  qaddcl  9826  qmulcl  9828  qreccl  9833  rpaddcl  9869  ge0addcl  10173  ge0xaddcl  10175  expge1  10793  rexanuz  11494  amgm2  11624  iooinsup  11783  mulcn2  11818  dvds2ln  12330  opoe  12401  omoe  12402  opeo  12403  omeo  12404  lcmgcd  12595  lcmdvds  12596  pc2dvds  12848  tgcl  14732  innei  14831  txbas  14926  txss12  14934  txbasval  14935  blsscls2  15161  qtopbasss  15189  lgslem3  15675  bj-indind  16253