Theorem an4s 592

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 588	. 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  593  anandis  596  anandirs  597  trin2  5128  fnun  5438  2elresin  5443  f1co  5554  f1oun  5603  f1oco  5606  f1mpt  5912  poxp  6397  tfrlem7  6483  brecop  6794  th3qlem1  6806  oviec  6810  pmss12g  6844  addcmpblnq  7587  mulcmpblnq  7588  mulpipqqs  7593  mulclnq  7596  mulcanenq  7605  distrnqg  7607  mulcmpblnq0  7664  mulcanenq0ec  7665  mulclnq0  7672  nqnq0a  7674  nqnq0m  7675  distrnq0  7679  genipv  7729  genpelvl  7732  genpelvu  7733  genpml  7737  genpmu  7738  genpcdl  7739  genpcuu  7740  genprndl  7741  genprndu  7742  distrlem1prl  7802  distrlem1pru  7803  ltsopr  7816  addcmpblnr  7959  ltsrprg  7967  addclsr  7973  mulclsr  7974  addasssrg  7976  addresr  8057  mulresr  8058  axaddass  8092  axmulass  8093  axdistr  8094  mulgt0  8254  mul4  8311  add4  8340  2addsub  8393  addsubeq4  8394  sub4  8424  muladd  8563  mulsub  8580  add20i  8672  mulge0i  8800  mulap0b  8835  divmuldivap  8892  ltmul12a  9040  zmulcl  9533  uz2mulcl  9842  qaddcl  9869  qmulcl  9871  qreccl  9876  rpaddcl  9912  ge0addcl  10216  ge0xaddcl  10218  expge1  10839  rexanuz  11553  amgm2  11683  iooinsup  11842  mulcn2  11877  dvds2ln  12390  opoe  12461  omoe  12462  opeo  12463  omeo  12464  lcmgcd  12655  lcmdvds  12656  pc2dvds  12908  tgcl  14794  innei  14893  txbas  14988  txss12  14996  txbasval  14997  blsscls2  15223  qtopbasss  15251  lgslem3  15737  bj-indind  16553