Theorem an32s 535

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 529	. 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  538  anabss1  543  fssres  5186  foco  5243  fun11iun  5274  fconstfvm  5515  isocnv  5590  f1oiso  5605  f1ocnvfv3  5641  tfrcl  6129  mapxpen  6564  findcard  6604  exmidfodomrlemim  6827  genpassl  7083  genpassu  7084  cnegexlem3  7659  recexaplem2  8121  divap0  8151  dfinfre  8417  qreccl  9127  xrlttr  9265  addmodlteq  9805  cau3lem  10547  climcn1  10697  climcn2  10698  climcaucn  10740  rplpwr  11294  dvdssq  11298  nn0seqcvgd  11301  lcmgcdlem  11337  isprm6  11404  phiprmpw  11476  cncfco  11647