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  5450  foco  5508  fun11iun  5542  fconstfvm  5801  isocnv  5879  f1oiso  5894  f1ocnvfv3  5932  tfrcl  6449  mapxpen  6944  findcard  6984  exmidfodomrlemim  7308  genpassl  7636  genpassu  7637  axsuploc  8144  cnegexlem3  8248  recexaplem2  8724  divap0  8756  dfinfre  9028  qreccl  9762  xrlttr  9916  addmodlteq  10541  cau3lem  11367  climcn1  11561  climcn2  11562  climcaucn  11604  ntrivcvgap  11801  rplpwr  12290  dvdssq  12294  nn0seqcvgd  12305  lcmgcdlem  12341  isprm6  12411  phiprmpw  12486  pcneg  12590  prmpwdvds  12620  4sqlem19  12674  grpinveu  13312  mulgnn0subcl  13413  mulgsubcl  13414  mhmmulg  13441  ghmmulg  13534  ringrghm  13766  dvdsrcl2  13803  crngunit  13815  dvdsrpropdg  13851  lss1d  14087  quscrng  14237  mulgghm2  14312  tgcl  14478  innei  14577  cncnp  14644  cnnei  14646  elbl2ps  14806  elbl2  14807  cncfco  15005  cnlimc  15086