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  5135  fnun  5445  2elresin  5450  f1co  5563  f1oun  5612  f1oco  5615  f1mpt  5922  poxp  6406  tfrlem7  6526  brecop  6837  th3qlem1  6849  oviec  6853  pmss12g  6887  addcmpblnq  7630  mulcmpblnq  7631  mulpipqqs  7636  mulclnq  7639  mulcanenq  7648  distrnqg  7650  mulcmpblnq0  7707  mulcanenq0ec  7708  mulclnq0  7715  nqnq0a  7717  nqnq0m  7718  distrnq0  7722  genipv  7772  genpelvl  7775  genpelvu  7776  genpml  7780  genpmu  7781  genpcdl  7782  genpcuu  7783  genprndl  7784  genprndu  7785  distrlem1prl  7845  distrlem1pru  7846  ltsopr  7859  addcmpblnr  8002  ltsrprg  8010  addclsr  8016  mulclsr  8017  addasssrg  8019  addresr  8100  mulresr  8101  axaddass  8135  axmulass  8136  axdistr  8137  mulgt0  8296  mul4  8353  add4  8382  2addsub  8435  addsubeq4  8436  sub4  8466  muladd  8605  mulsub  8622  add20i  8714  mulge0i  8842  mulap0b  8877  divmuldivap  8934  ltmul12a  9082  zmulcl  9577  uz2mulcl  9886  qaddcl  9913  qmulcl  9915  qreccl  9920  rpaddcl  9956  ge0addcl  10260  ge0xaddcl  10262  expge1  10884  rexanuz  11611  amgm2  11741  iooinsup  11900  mulcn2  11935  dvds2ln  12448  opoe  12519  omoe  12520  opeo  12521  omeo  12522  lcmgcd  12713  lcmdvds  12714  pc2dvds  12966  tgcl  14858  innei  14957  txbas  15052  txss12  15060  txbasval  15061  blsscls2  15287  qtopbasss  15315  lgslem3  15804  bj-indind  16631