Theorem an4s 588

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  589  anandis  592  anandirs  593  trin2  5057  fnun  5360  2elresin  5365  f1co  5471  f1oun  5520  f1oco  5523  f1mpt  5814  poxp  6285  tfrlem7  6370  brecop  6679  th3qlem1  6691  oviec  6695  pmss12g  6729  addcmpblnq  7427  mulcmpblnq  7428  mulpipqqs  7433  mulclnq  7436  mulcanenq  7445  distrnqg  7447  mulcmpblnq0  7504  mulcanenq0ec  7505  mulclnq0  7512  nqnq0a  7514  nqnq0m  7515  distrnq0  7519  genipv  7569  genpelvl  7572  genpelvu  7573  genpml  7577  genpmu  7578  genpcdl  7579  genpcuu  7580  genprndl  7581  genprndu  7582  distrlem1prl  7642  distrlem1pru  7643  ltsopr  7656  addcmpblnr  7799  ltsrprg  7807  addclsr  7813  mulclsr  7814  addasssrg  7816  addresr  7897  mulresr  7898  axaddass  7932  axmulass  7933  axdistr  7934  mulgt0  8094  mul4  8151  add4  8180  2addsub  8233  addsubeq4  8234  sub4  8264  muladd  8403  mulsub  8420  add20i  8511  mulge0i  8639  mulap0b  8674  divmuldivap  8731  ltmul12a  8879  zmulcl  9370  uz2mulcl  9673  qaddcl  9700  qmulcl  9702  qreccl  9707  rpaddcl  9743  ge0addcl  10047  ge0xaddcl  10049  expge1  10647  rexanuz  11132  amgm2  11262  iooinsup  11420  mulcn2  11455  dvds2ln  11967  opoe  12036  omoe  12037  opeo  12038  omeo  12039  lcmgcd  12216  lcmdvds  12217  pc2dvds  12468  tgcl  14232  innei  14331  txbas  14426  txss12  14434  txbasval  14435  blsscls2  14661  qtopbasss  14689  lgslem3  15118  bj-indind  15424