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  616  fssres  5509  foco  5567  fun11iun  5601  fconstfvm  5867  isocnv  5947  f1oiso  5962  f1ocnvfv3  6002  tfrcl  6525  mapxpen  7029  findcard  7070  exmidfodomrlemim  7402  genpassl  7734  genpassu  7735  axsuploc  8242  cnegexlem3  8346  recexaplem2  8822  divap0  8854  dfinfre  9126  qreccl  9866  xrlttr  10020  addmodlteq  10650  cau3lem  11665  climcn1  11859  climcn2  11860  climcaucn  11902  ntrivcvgap  12099  rplpwr  12588  dvdssq  12592  nn0seqcvgd  12603  lcmgcdlem  12639  isprm6  12709  phiprmpw  12784  pcneg  12888  prmpwdvds  12918  4sqlem19  12972  grpinveu  13611  mulgnn0subcl  13712  mulgsubcl  13713  mhmmulg  13740  ghmmulg  13833  ringrghm  14065  dvdsrcl2  14103  crngunit  14115  dvdsrpropdg  14151  lss1d  14387  quscrng  14537  mulgghm2  14612  tgcl  14778  innei  14877  cncnp  14944  cnnei  14946  elbl2ps  15106  elbl2  15107  cncfco  15305  cnlimc  15386