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  5520  foco  5579  fun11iun  5613  fconstfvm  5880  isocnv  5962  f1oiso  5977  f1ocnvfv3  6017  tfrcl  6573  mapxpen  7077  findcard  7120  exmidfodomrlemim  7455  genpassl  7787  genpassu  7788  axsuploc  8294  cnegexlem3  8398  recexaplem2  8874  divap0  8906  dfinfre  9178  qreccl  9920  xrlttr  10074  addmodlteq  10706  cau3lem  11737  climcn1  11931  climcn2  11932  climcaucn  11974  ntrivcvgap  12172  rplpwr  12661  dvdssq  12665  nn0seqcvgd  12676  lcmgcdlem  12712  isprm6  12782  phiprmpw  12857  pcneg  12961  prmpwdvds  12991  4sqlem19  13045  grpinveu  13684  mulgnn0subcl  13785  mulgsubcl  13786  mhmmulg  13813  ghmmulg  13906  ringrghm  14139  dvdsrcl2  14177  crngunit  14189  dvdsrpropdg  14225  lss1d  14462  quscrng  14612  mulgghm2  14687  tgcl  14858  innei  14957  cncnp  15024  cnnei  15026  elbl2ps  15186  elbl2  15187  cncfco  15385  cnlimc  15466