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  5073  fnun  5381  2elresin  5386  f1co  5492  f1oun  5541  f1oco  5544  f1mpt  5839  poxp  6317  tfrlem7  6402  brecop  6711  th3qlem1  6723  oviec  6727  pmss12g  6761  addcmpblnq  7479  mulcmpblnq  7480  mulpipqqs  7485  mulclnq  7488  mulcanenq  7497  distrnqg  7499  mulcmpblnq0  7556  mulcanenq0ec  7557  mulclnq0  7564  nqnq0a  7566  nqnq0m  7567  distrnq0  7571  genipv  7621  genpelvl  7624  genpelvu  7625  genpml  7629  genpmu  7630  genpcdl  7631  genpcuu  7632  genprndl  7633  genprndu  7634  distrlem1prl  7694  distrlem1pru  7695  ltsopr  7708  addcmpblnr  7851  ltsrprg  7859  addclsr  7865  mulclsr  7866  addasssrg  7868  addresr  7949  mulresr  7950  axaddass  7984  axmulass  7985  axdistr  7986  mulgt0  8146  mul4  8203  add4  8232  2addsub  8285  addsubeq4  8286  sub4  8316  muladd  8455  mulsub  8472  add20i  8564  mulge0i  8692  mulap0b  8727  divmuldivap  8784  ltmul12a  8932  zmulcl  9425  uz2mulcl  9728  qaddcl  9755  qmulcl  9757  qreccl  9762  rpaddcl  9798  ge0addcl  10102  ge0xaddcl  10104  expge1  10719  rexanuz  11241  amgm2  11371  iooinsup  11530  mulcn2  11565  dvds2ln  12077  opoe  12148  omoe  12149  opeo  12150  omeo  12151  lcmgcd  12342  lcmdvds  12343  pc2dvds  12595  tgcl  14478  innei  14577  txbas  14672  txss12  14680  txbasval  14681  blsscls2  14907  qtopbasss  14935  lgslem3  15421  bj-indind  15801