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  5093  fnun  5401  2elresin  5406  f1co  5515  f1oun  5564  f1oco  5567  f1mpt  5863  poxp  6341  tfrlem7  6426  brecop  6735  th3qlem1  6747  oviec  6751  pmss12g  6785  addcmpblnq  7515  mulcmpblnq  7516  mulpipqqs  7521  mulclnq  7524  mulcanenq  7533  distrnqg  7535  mulcmpblnq0  7592  mulcanenq0ec  7593  mulclnq0  7600  nqnq0a  7602  nqnq0m  7603  distrnq0  7607  genipv  7657  genpelvl  7660  genpelvu  7661  genpml  7665  genpmu  7666  genpcdl  7667  genpcuu  7668  genprndl  7669  genprndu  7670  distrlem1prl  7730  distrlem1pru  7731  ltsopr  7744  addcmpblnr  7887  ltsrprg  7895  addclsr  7901  mulclsr  7902  addasssrg  7904  addresr  7985  mulresr  7986  axaddass  8020  axmulass  8021  axdistr  8022  mulgt0  8182  mul4  8239  add4  8268  2addsub  8321  addsubeq4  8322  sub4  8352  muladd  8491  mulsub  8508  add20i  8600  mulge0i  8728  mulap0b  8763  divmuldivap  8820  ltmul12a  8968  zmulcl  9461  uz2mulcl  9764  qaddcl  9791  qmulcl  9793  qreccl  9798  rpaddcl  9834  ge0addcl  10138  ge0xaddcl  10140  expge1  10758  rexanuz  11414  amgm2  11544  iooinsup  11703  mulcn2  11738  dvds2ln  12250  opoe  12321  omoe  12322  opeo  12323  omeo  12324  lcmgcd  12515  lcmdvds  12516  pc2dvds  12768  tgcl  14651  innei  14750  txbas  14845  txss12  14853  txbasval  14854  blsscls2  15080  qtopbasss  15108  lgslem3  15594  bj-indind  16067