Theorem an32s 533

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 527	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 119	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anass1rs  536  anabss1  541  fssres  5134  foco  5190  fun11iun  5221  fconstfvm  5454  isocnv  5529  f1oiso  5543  f1ocnvfv3  5579  tfrcl  6060  mapxpen  6493  findcard  6533  exmidfodomrlemim  6729  genpassl  6985  genpassu  6986  cnegexlem3  7561  recexaplem2  8018  divap0  8048  dfinfre  8310  qreccl  9021  xrlttr  9159  addmodlteq  9693  cau3lem  10373  climcn1  10520  climcn2  10521  climcaucn  10561  rplpwr  10795  dvdssq  10799  nn0seqcvgd  10802  lcmgcdlem  10838  isprm6  10905  phiprmpw  10977