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  5062  fnun  5367  2elresin  5372  f1co  5478  f1oun  5527  f1oco  5530  f1mpt  5821  poxp  6299  tfrlem7  6384  brecop  6693  th3qlem1  6705  oviec  6709  pmss12g  6743  addcmpblnq  7453  mulcmpblnq  7454  mulpipqqs  7459  mulclnq  7462  mulcanenq  7471  distrnqg  7473  mulcmpblnq0  7530  mulcanenq0ec  7531  mulclnq0  7538  nqnq0a  7540  nqnq0m  7541  distrnq0  7545  genipv  7595  genpelvl  7598  genpelvu  7599  genpml  7603  genpmu  7604  genpcdl  7605  genpcuu  7606  genprndl  7607  genprndu  7608  distrlem1prl  7668  distrlem1pru  7669  ltsopr  7682  addcmpblnr  7825  ltsrprg  7833  addclsr  7839  mulclsr  7840  addasssrg  7842  addresr  7923  mulresr  7924  axaddass  7958  axmulass  7959  axdistr  7960  mulgt0  8120  mul4  8177  add4  8206  2addsub  8259  addsubeq4  8260  sub4  8290  muladd  8429  mulsub  8446  add20i  8538  mulge0i  8666  mulap0b  8701  divmuldivap  8758  ltmul12a  8906  zmulcl  9398  uz2mulcl  9701  qaddcl  9728  qmulcl  9730  qreccl  9735  rpaddcl  9771  ge0addcl  10075  ge0xaddcl  10077  expge1  10687  rexanuz  11172  amgm2  11302  iooinsup  11461  mulcn2  11496  dvds2ln  12008  opoe  12079  omoe  12080  opeo  12081  omeo  12082  lcmgcd  12273  lcmdvds  12274  pc2dvds  12526  tgcl  14408  innei  14507  txbas  14602  txss12  14610  txbasval  14611  blsscls2  14837  qtopbasss  14865  lgslem3  15351  bj-indind  15686