Theorem an32s 568

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anass1rs  571  anabss1  576  biadanid  616  fssres  5500  foco  5558  fun11iun  5592  fconstfvm  5856  isocnv  5934  f1oiso  5949  f1ocnvfv3  5989  tfrcl  6508  mapxpen  7005  findcard  7046  exmidfodomrlemim  7375  genpassl  7707  genpassu  7708  axsuploc  8215  cnegexlem3  8319  recexaplem2  8795  divap0  8827  dfinfre  9099  qreccl  9833  xrlttr  9987  addmodlteq  10615  cau3lem  11620  climcn1  11814  climcn2  11815  climcaucn  11857  ntrivcvgap  12054  rplpwr  12543  dvdssq  12547  nn0seqcvgd  12558  lcmgcdlem  12594  isprm6  12664  phiprmpw  12739  pcneg  12843  prmpwdvds  12873  4sqlem19  12927  grpinveu  13566  mulgnn0subcl  13667  mulgsubcl  13668  mhmmulg  13695  ghmmulg  13788  ringrghm  14020  dvdsrcl2  14057  crngunit  14069  dvdsrpropdg  14105  lss1d  14341  quscrng  14491  mulgghm2  14566  tgcl  14732  innei  14831  cncnp  14898  cnnei  14900  elbl2ps  15060  elbl2  15061  cncfco  15259  cnlimc  15340