Theorem an4s 578

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an42s  579  anandis  582  anandirs  583  trin2  4989  fnun  5288  2elresin  5293  f1co  5399  f1oun  5446  f1oco  5449  f1mpt  5733  poxp  6191  tfrlem7  6276  brecop  6582  th3qlem1  6594  oviec  6598  pmss12g  6632  addcmpblnq  7299  mulcmpblnq  7300  mulpipqqs  7305  mulclnq  7308  mulcanenq  7317  distrnqg  7319  mulcmpblnq0  7376  mulcanenq0ec  7377  mulclnq0  7384  nqnq0a  7386  nqnq0m  7387  distrnq0  7391  genipv  7441  genpelvl  7444  genpelvu  7445  genpml  7449  genpmu  7450  genpcdl  7451  genpcuu  7452  genprndl  7453  genprndu  7454  distrlem1prl  7514  distrlem1pru  7515  ltsopr  7528  addcmpblnr  7671  ltsrprg  7679  addclsr  7685  mulclsr  7686  addasssrg  7688  addresr  7769  mulresr  7770  axaddass  7804  axmulass  7805  axdistr  7806  mulgt0  7964  mul4  8021  add4  8050  2addsub  8103  addsubeq4  8104  sub4  8134  muladd  8273  mulsub  8290  add20i  8381  mulge0i  8509  mulap0b  8543  divmuldivap  8599  ltmul12a  8746  zmulcl  9235  uz2mulcl  9537  qaddcl  9564  qmulcl  9566  qreccl  9571  rpaddcl  9604  ge0addcl  9908  ge0xaddcl  9910  expge1  10482  rexanuz  10916  amgm2  11046  iooinsup  11204  mulcn2  11239  dvds2ln  11750  opoe  11817  omoe  11818  opeo  11819  omeo  11820  lcmgcd  11989  lcmdvds  11990  pc2dvds  12238  tgcl  12605  innei  12704  txbas  12799  txss12  12807  txbasval  12808  blsscls2  13034  qtopbasss  13062  bj-indind  13649