Theorem an4s 588

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 586	. 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  589  anandis  592  anandirs  593  trin2  5021  fnun  5323  2elresin  5328  f1co  5434  f1oun  5482  f1oco  5485  f1mpt  5772  poxp  6233  tfrlem7  6318  brecop  6625  th3qlem1  6637  oviec  6641  pmss12g  6675  addcmpblnq  7366  mulcmpblnq  7367  mulpipqqs  7372  mulclnq  7375  mulcanenq  7384  distrnqg  7386  mulcmpblnq0  7443  mulcanenq0ec  7444  mulclnq0  7451  nqnq0a  7453  nqnq0m  7454  distrnq0  7458  genipv  7508  genpelvl  7511  genpelvu  7512  genpml  7516  genpmu  7517  genpcdl  7518  genpcuu  7519  genprndl  7520  genprndu  7521  distrlem1prl  7581  distrlem1pru  7582  ltsopr  7595  addcmpblnr  7738  ltsrprg  7746  addclsr  7752  mulclsr  7753  addasssrg  7755  addresr  7836  mulresr  7837  axaddass  7871  axmulass  7872  axdistr  7873  mulgt0  8032  mul4  8089  add4  8118  2addsub  8171  addsubeq4  8172  sub4  8202  muladd  8341  mulsub  8358  add20i  8449  mulge0i  8577  mulap0b  8612  divmuldivap  8669  ltmul12a  8817  zmulcl  9306  uz2mulcl  9608  qaddcl  9635  qmulcl  9637  qreccl  9642  rpaddcl  9677  ge0addcl  9981  ge0xaddcl  9983  expge1  10557  rexanuz  10997  amgm2  11127  iooinsup  11285  mulcn2  11320  dvds2ln  11831  opoe  11900  omoe  11901  opeo  11902  omeo  11903  lcmgcd  12078  lcmdvds  12079  pc2dvds  12329  tgcl  13567  innei  13666  txbas  13761  txss12  13769  txbasval  13770  blsscls2  13996  qtopbasss  14024  lgslem3  14406  bj-indind  14687