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  5545  foco  5606  fun11iun  5640  fconstfvm  5907  isocnv  5990  f1oiso  6005  f1ocnvfv3  6047  tfrcl  6608  mapxpen  7114  findcard  7158  exmidfodomrlemim  7517  genpassl  7855  genpassu  7856  axsuploc  8362  cnegexlem3  8466  recexaplem2  8943  divap0  8975  dfinfre  9247  qreccl  9992  xrlttr  10147  addmodlteq  10784  cau3lem  11824  climcn1  12018  climcn2  12019  climcaucn  12061  ntrivcvgap  12259  rplpwr  12748  dvdssq  12752  nn0seqcvgd  12763  lcmgcdlem  12799  isprm6  12869  phiprmpw  12944  pcneg  13048  prmpwdvds  13078  4sqlem19  13132  grpinveu  13793  mulgnn0subcl  13888  mulgsubcl  13889  mhmmulg  13916  ghmmulg  14009  ringrghm  14305  dvdsrcl2  14344  crngunit  14356  dvdsrpropdg  14392  lss1d  14657  quscrng  14807  mulgghm2  14882  tgcl  15055  innei  15154  cncnp  15221  cnnei  15223  elbl2ps  15383  elbl2  15384  cncfco  15582  cnlimc  15663