Theorem an32s 570

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 564	. 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  573  anabss1  578  biadanid  618  fssres  5512  foco  5570  fun11iun  5604  fconstfvm  5872  isocnv  5952  f1oiso  5967  f1ocnvfv3  6007  tfrcl  6530  mapxpen  7034  findcard  7077  exmidfodomrlemim  7412  genpassl  7744  genpassu  7745  axsuploc  8252  cnegexlem3  8356  recexaplem2  8832  divap0  8864  dfinfre  9136  qreccl  9876  xrlttr  10030  addmodlteq  10661  cau3lem  11679  climcn1  11873  climcn2  11874  climcaucn  11916  ntrivcvgap  12114  rplpwr  12603  dvdssq  12607  nn0seqcvgd  12618  lcmgcdlem  12654  isprm6  12724  phiprmpw  12799  pcneg  12903  prmpwdvds  12933  4sqlem19  12987  grpinveu  13626  mulgnn0subcl  13727  mulgsubcl  13728  mhmmulg  13755  ghmmulg  13848  ringrghm  14081  dvdsrcl2  14119  crngunit  14131  dvdsrpropdg  14167  lss1d  14403  quscrng  14553  mulgghm2  14628  tgcl  14794  innei  14893  cncnp  14960  cnnei  14962  elbl2ps  15122  elbl2  15123  cncfco  15321  cnlimc  15402