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  5871  isocnv  5951  f1oiso  5966  f1ocnvfv3  6006  tfrcl  6529  mapxpen  7033  findcard  7076  exmidfodomrlemim  7411  genpassl  7743  genpassu  7744  axsuploc  8251  cnegexlem3  8355  recexaplem2  8831  divap0  8863  dfinfre  9135  qreccl  9875  xrlttr  10029  addmodlteq  10659  cau3lem  11674  climcn1  11868  climcn2  11869  climcaucn  11911  ntrivcvgap  12108  rplpwr  12597  dvdssq  12601  nn0seqcvgd  12612  lcmgcdlem  12648  isprm6  12718  phiprmpw  12793  pcneg  12897  prmpwdvds  12927  4sqlem19  12981  grpinveu  13620  mulgnn0subcl  13721  mulgsubcl  13722  mhmmulg  13749  ghmmulg  13842  ringrghm  14074  dvdsrcl2  14112  crngunit  14124  dvdsrpropdg  14160  lss1d  14396  quscrng  14546  mulgghm2  14621  tgcl  14787  innei  14886  cncnp  14953  cnnei  14955  elbl2ps  15115  elbl2  15116  cncfco  15314  cnlimc  15395