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  5345  foco  5402  fun11iun  5435  fconstfvm  5685  isocnv  5761  f1oiso  5776  f1ocnvfv3  5813  tfrcl  6311  mapxpen  6793  findcard  6833  exmidfodomrlemim  7136  genpassl  7444  genpassu  7445  axsuploc  7950  cnegexlem3  8052  recexaplem2  8526  divap0  8557  dfinfre  8827  qreccl  9551  xrlttr  9702  addmodlteq  10297  cau3lem  11014  climcn1  11205  climcn2  11206  climcaucn  11248  ntrivcvgap  11445  rplpwr  11911  dvdssq  11915  nn0seqcvgd  11918  lcmgcdlem  11954  isprm6  12022  phiprmpw  12097  tgcl  12475  innei  12574  cncnp  12641  cnnei  12643  elbl2ps  12803  elbl2  12804  cncfco  12989  cnlimc  13052