Theorem an32s 568

Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)

Hypothesis

Ref	Expression
an32s.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
an32s	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Proof of Theorem an32s

Step	Hyp	Ref	Expression
1		an32 562	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.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:  anass1rs  571  anabss1  576  biadanid  616  fssres  5503  foco  5561  fun11iun  5595  fconstfvm  5861  isocnv  5941  f1oiso  5956  f1ocnvfv3  5996  tfrcl  6516  mapxpen  7017  findcard  7058  exmidfodomrlemim  7390  genpassl  7722  genpassu  7723  axsuploc  8230  cnegexlem3  8334  recexaplem2  8810  divap0  8842  dfinfre  9114  qreccl  9849  xrlttr  10003  addmodlteq  10632  cau3lem  11640  climcn1  11834  climcn2  11835  climcaucn  11877  ntrivcvgap  12074  rplpwr  12563  dvdssq  12567  nn0seqcvgd  12578  lcmgcdlem  12614  isprm6  12684  phiprmpw  12759  pcneg  12863  prmpwdvds  12893  4sqlem19  12947  grpinveu  13586  mulgnn0subcl  13687  mulgsubcl  13688  mhmmulg  13715  ghmmulg  13808  ringrghm  14040  dvdsrcl2  14078  crngunit  14090  dvdsrpropdg  14126  lss1d  14362  quscrng  14512  mulgghm2  14587  tgcl  14753  innei  14852  cncnp  14919  cnnei  14921  elbl2ps  15081  elbl2  15082  cncfco  15280  cnlimc  15361