Theorem an4s 577

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 575	. 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  578  anandis  581  anandirs  582  trin2  4925  fnun  5224  2elresin  5229  f1co  5335  f1oun  5380  f1oco  5383  f1mpt  5665  poxp  6122  tfrlem7  6207  brecop  6512  th3qlem1  6524  oviec  6528  pmss12g  6562  addcmpblnq  7168  mulcmpblnq  7169  mulpipqqs  7174  mulclnq  7177  mulcanenq  7186  distrnqg  7188  mulcmpblnq0  7245  mulcanenq0ec  7246  mulclnq0  7253  nqnq0a  7255  nqnq0m  7256  distrnq0  7260  genipv  7310  genpelvl  7313  genpelvu  7314  genpml  7318  genpmu  7319  genpcdl  7320  genpcuu  7321  genprndl  7322  genprndu  7323  distrlem1prl  7383  distrlem1pru  7384  ltsopr  7397  addcmpblnr  7540  ltsrprg  7548  addclsr  7554  mulclsr  7555  addasssrg  7557  addresr  7638  mulresr  7639  axaddass  7673  axmulass  7674  axdistr  7675  mulgt0  7832  mul4  7887  add4  7916  2addsub  7969  addsubeq4  7970  sub4  8000  muladd  8139  mulsub  8156  add20i  8247  mulge0i  8375  mulap0b  8409  divmuldivap  8465  ltmul12a  8611  zmulcl  9100  uz2mulcl  9395  qaddcl  9420  qmulcl  9422  qreccl  9427  rpaddcl  9458  ge0addcl  9757  ge0xaddcl  9759  expge1  10323  rexanuz  10753  amgm2  10883  iooinsup  11039  mulcn2  11074  dvds2ln  11515  opoe  11581  omoe  11582  opeo  11583  omeo  11584  lcmgcd  11748  lcmdvds  11749  tgcl  12222  innei  12321  txbas  12416  txss12  12424  txbasval  12425  blsscls2  12651  qtopbasss  12679  bj-indind  13119