Theorem an32s 532

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 526	. 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  535  anabss1  540  fssres  5086  foco  5136  fun11iun  5167  fconstfvm  5400  isocnv  5471  f1oiso  5485  f1ocnvfv3  5521  findcard  6372  genpassl  6714  genpassu  6715  cnegexlem3  7285  recexaplem2  7742  divap0  7772  dfinfre  8034  qreccl  8727  xrlttr  8870  addmodlteq  9400  cau3lem  10000  climcn1  10147  climcn2  10148  climcaucn  10188  rplpwr  10416  dvdssq  10420  nn0seqcvgd  10423  lcmgcdlem  10459  isprm6  10526