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  5058  fnun  5361  2elresin  5366  f1co  5472  f1oun  5521  f1oco  5524  f1mpt  5815  poxp  6287  tfrlem7  6372  brecop  6681  th3qlem1  6693  oviec  6697  pmss12g  6731  addcmpblnq  7429  mulcmpblnq  7430  mulpipqqs  7435  mulclnq  7438  mulcanenq  7447  distrnqg  7449  mulcmpblnq0  7506  mulcanenq0ec  7507  mulclnq0  7514  nqnq0a  7516  nqnq0m  7517  distrnq0  7521  genipv  7571  genpelvl  7574  genpelvu  7575  genpml  7579  genpmu  7580  genpcdl  7581  genpcuu  7582  genprndl  7583  genprndu  7584  distrlem1prl  7644  distrlem1pru  7645  ltsopr  7658  addcmpblnr  7801  ltsrprg  7809  addclsr  7815  mulclsr  7816  addasssrg  7818  addresr  7899  mulresr  7900  axaddass  7934  axmulass  7935  axdistr  7936  mulgt0  8096  mul4  8153  add4  8182  2addsub  8235  addsubeq4  8236  sub4  8266  muladd  8405  mulsub  8422  add20i  8513  mulge0i  8641  mulap0b  8676  divmuldivap  8733  ltmul12a  8881  zmulcl  9373  uz2mulcl  9676  qaddcl  9703  qmulcl  9705  qreccl  9710  rpaddcl  9746  ge0addcl  10050  ge0xaddcl  10052  expge1  10650  rexanuz  11135  amgm2  11265  iooinsup  11423  mulcn2  11458  dvds2ln  11970  opoe  12039  omoe  12040  opeo  12041  omeo  12042  lcmgcd  12219  lcmdvds  12220  pc2dvds  12471  tgcl  14243  innei  14342  txbas  14437  txss12  14445  txbasval  14446  blsscls2  14672  qtopbasss  14700  lgslem3  15159  bj-indind  15494