Theorem an4s 596

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 592	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 121	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an42s  597  anandis  600  anandirs  601  trin2  5182  fnun  5492  2elresin  5497  f1co  5613  f1oun  5662  f1oco  5665  f1mpt  5980  poxp  6472  tfrlem7  6592  brecop  6903  th3qlem1  6915  oviec  6919  pmss12g  6960  addcmpblnq  7740  mulcmpblnq  7741  mulpipqqs  7746  mulclnq  7749  mulcanenq  7758  distrnqg  7760  mulcmpblnq0  7817  mulcanenq0ec  7818  mulclnq0  7825  nqnq0a  7827  nqnq0m  7828  distrnq0  7832  genipv  7882  genpelvl  7885  genpelvu  7886  genpml  7890  genpmu  7891  genpcdl  7892  genpcuu  7893  genprndl  7894  genprndu  7895  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  addcmpblnr  8112  ltsrprg  8120  addclsr  8126  mulclsr  8127  addasssrg  8129  addresr  8210  mulresr  8211  axaddass  8245  axmulass  8246  axdistr  8247  mulgt0  8406  mul4  8465  add4  8494  2addsub  8547  addsubeq4  8548  sub4  8578  muladd  8718  mulsub  8735  add20i  8827  mulge0i  8956  mulap0b  8991  divmuldivap  9050  ltmul12a  9198  zmulcl  9709  uz2mulcl  10024  qaddcl  10051  qmulcl  10053  qreccl  10058  rpaddcl  10095  ge0addcl  10400  ge0xaddcl  10402  expge1  11034  rexanuz  11776  amgm2  11907  iooinsup  12068  mulcn2  12103  dvds2ln  12616  opoe  12687  omoe  12688  opeo  12689  omeo  12690  lcmgcd  12881  lcmdvds  12882  pc2dvds  13138  tgcl  15290  innei  15389  txbas  15484  txss12  15492  txbasval  15493  blsscls2  15719  qtopbasss  15747  lgslem3  16326  bj-indind  17163