Theorem an4s 522

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  an42s  523  anandis  526  anandirs  527  trin2  4716  fnun  5005  2elresin  5010  f1co  5101  f1oun  5146  f1oco  5149  f1mpt  5410  poxp  5853  tfrlem7  5933  brecop  6196  th3qlem1  6208  oviec  6212  addcmpblnq  6465  mulcmpblnq  6466  mulpipqqs  6471  mulclnq  6474  mulcanenq  6483  distrnqg  6485  mulcmpblnq0  6542  mulcanenq0ec  6543  mulclnq0  6550  nqnq0a  6552  nqnq0m  6553  distrnq0  6557  genipv  6607  genpelvl  6610  genpelvu  6611  genpml  6615  genpmu  6616  genpcdl  6617  genpcuu  6618  genprndl  6619  genprndu  6620  distrlem1prl  6680  distrlem1pru  6681  ltsopr  6694  addcmpblnr  6824  ltsrprg  6832  addclsr  6838  mulclsr  6839  addasssrg  6841  addresr  6913  mulresr  6914  axaddass  6946  axmulass  6947  axdistr  6948  mulgt0  7093  mul4  7145  add4  7172  2addsub  7225  addsubeq4  7226  sub4  7256  muladd  7381  mulsub  7398  add20i  7484  mulge0i  7611  mulap0b  7636  divmuldivap  7688  ltmul12a  7826  zmulcl  8297  uz2mulcl  8545  qaddcl  8570  qmulcl  8572  qreccl  8576  rpaddcl  8606  ge0addcl  8850  serige0  9252  expge1  9292  rexanuz  9587  amgm2  9714  mulcn2  9833  bj-indind  10056