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  614  fssres  5445  foco  5503  fun11iun  5537  fconstfvm  5792  isocnv  5870  f1oiso  5885  f1ocnvfv3  5923  tfrcl  6440  mapxpen  6927  findcard  6967  exmidfodomrlemim  7291  genpassl  7619  genpassu  7620  axsuploc  8127  cnegexlem3  8231  recexaplem2  8707  divap0  8739  dfinfre  9011  qreccl  9745  xrlttr  9899  addmodlteq  10524  cau3lem  11344  climcn1  11538  climcn2  11539  climcaucn  11581  ntrivcvgap  11778  rplpwr  12267  dvdssq  12271  nn0seqcvgd  12282  lcmgcdlem  12318  isprm6  12388  phiprmpw  12463  pcneg  12567  prmpwdvds  12597  4sqlem19  12651  grpinveu  13288  mulgnn0subcl  13389  mulgsubcl  13390  mhmmulg  13417  ghmmulg  13510  ringrghm  13742  dvdsrcl2  13779  crngunit  13791  dvdsrpropdg  13827  lss1d  14063  quscrng  14213  mulgghm2  14288  tgcl  14454  innei  14553  cncnp  14620  cnnei  14622  elbl2ps  14782  elbl2  14783  cncfco  14981  cnlimc  15062