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  7451  mulcmpblnq  7452  mulpipqqs  7457  mulclnq  7460  mulcanenq  7469  distrnqg  7471  mulcmpblnq0  7528  mulcanenq0ec  7529  mulclnq0  7536  nqnq0a  7538  nqnq0m  7539  distrnq0  7543  genipv  7593  genpelvl  7596  genpelvu  7597  genpml  7601  genpmu  7602  genpcdl  7603  genpcuu  7604  genprndl  7605  genprndu  7606  distrlem1prl  7666  distrlem1pru  7667  ltsopr  7680  addcmpblnr  7823  ltsrprg  7831  addclsr  7837  mulclsr  7838  addasssrg  7840  addresr  7921  mulresr  7922  axaddass  7956  axmulass  7957  axdistr  7958  mulgt0  8118  mul4  8175  add4  8204  2addsub  8257  addsubeq4  8258  sub4  8288  muladd  8427  mulsub  8444  add20i  8536  mulge0i  8664  mulap0b  8699  divmuldivap  8756  ltmul12a  8904  zmulcl  9396  uz2mulcl  9699  qaddcl  9726  qmulcl  9728  qreccl  9733  rpaddcl  9769  ge0addcl  10073  ge0xaddcl  10075  expge1  10685  rexanuz  11170  amgm2  11300  iooinsup  11459  mulcn2  11494  dvds2ln  12006  opoe  12077  omoe  12078  opeo  12079  omeo  12080  lcmgcd  12271  lcmdvds  12272  pc2dvds  12524  tgcl  14384  innei  14483  txbas  14578  txss12  14586  txbasval  14587  blsscls2  14813  qtopbasss  14841  lgslem3  15327  bj-indind  15662