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  614  fssres  5436  foco  5494  fun11iun  5528  fconstfvm  5783  isocnv  5861  f1oiso  5876  f1ocnvfv3  5914  tfrcl  6431  mapxpen  6918  findcard  6958  exmidfodomrlemim  7282  genpassl  7610  genpassu  7611  axsuploc  8118  cnegexlem3  8222  recexaplem2  8698  divap0  8730  dfinfre  9002  qreccl  9735  xrlttr  9889  addmodlteq  10509  cau3lem  11298  climcn1  11492  climcn2  11493  climcaucn  11535  ntrivcvgap  11732  rplpwr  12221  dvdssq  12225  nn0seqcvgd  12236  lcmgcdlem  12272  isprm6  12342  phiprmpw  12417  pcneg  12521  prmpwdvds  12551  4sqlem19  12605  grpinveu  13242  mulgnn0subcl  13343  mulgsubcl  13344  mhmmulg  13371  ghmmulg  13464  ringrghm  13696  dvdsrcl2  13733  crngunit  13745  dvdsrpropdg  13781  lss1d  14017  quscrng  14167  mulgghm2  14242  tgcl  14408  innei  14507  cncnp  14574  cnnei  14576  elbl2ps  14736  elbl2  14737  cncfco  14935  cnlimc  15016