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  5540  foco  5601  fun11iun  5635  fconstfvm  5902  isocnv  5984  f1oiso  5999  f1ocnvfv3  6039  tfrcl  6595  mapxpen  7101  findcard  7145  exmidfodomrlemim  7504  genpassl  7839  genpassu  7840  axsuploc  8346  cnegexlem3  8450  recexaplem2  8926  divap0  8958  dfinfre  9230  qreccl  9974  xrlttr  10128  addmodlteq  10760  cau3lem  11799  climcn1  11993  climcn2  11994  climcaucn  12036  ntrivcvgap  12234  rplpwr  12723  dvdssq  12727  nn0seqcvgd  12738  lcmgcdlem  12774  isprm6  12844  phiprmpw  12919  pcneg  13023  prmpwdvds  13053  4sqlem19  13107  grpinveu  13751  mulgnn0subcl  13852  mulgsubcl  13853  mhmmulg  13880  ghmmulg  13973  ringrghm  14206  dvdsrcl2  14244  crngunit  14256  dvdsrpropdg  14292  lss1d  14531  quscrng  14681  mulgghm2  14756  tgcl  14929  innei  15028  cncnp  15095  cnnei  15097  elbl2ps  15257  elbl2  15258  cncfco  15456  cnlimc  15537