Theorem an32s 558

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 552	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.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:  anass1rs  561  anabss1  566  fssres  5306  foco  5363  fun11iun  5396  fconstfvm  5646  isocnv  5720  f1oiso  5735  f1ocnvfv3  5771  tfrcl  6269  mapxpen  6750  findcard  6790  exmidfodomrlemim  7074  genpassl  7356  genpassu  7357  axsuploc  7861  cnegexlem3  7963  recexaplem2  8437  divap0  8468  dfinfre  8738  qreccl  9461  xrlttr  9611  addmodlteq  10202  cau3lem  10918  climcn1  11109  climcn2  11110  climcaucn  11152  ntrivcvgap  11349  rplpwr  11751  dvdssq  11755  nn0seqcvgd  11758  lcmgcdlem  11794  isprm6  11861  phiprmpw  11934  tgcl  12272  innei  12371  cncnp  12438  cnnei  12440  elbl2ps  12600  elbl2  12601  cncfco  12786  cnlimc  12849