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  5463  foco  5521  fun11iun  5555  fconstfvm  5815  isocnv  5893  f1oiso  5908  f1ocnvfv3  5946  tfrcl  6463  mapxpen  6960  findcard  7000  exmidfodomrlemim  7325  genpassl  7657  genpassu  7658  axsuploc  8165  cnegexlem3  8269  recexaplem2  8745  divap0  8777  dfinfre  9049  qreccl  9783  xrlttr  9937  addmodlteq  10565  cau3lem  11500  climcn1  11694  climcn2  11695  climcaucn  11737  ntrivcvgap  11934  rplpwr  12423  dvdssq  12427  nn0seqcvgd  12438  lcmgcdlem  12474  isprm6  12544  phiprmpw  12619  pcneg  12723  prmpwdvds  12753  4sqlem19  12807  grpinveu  13445  mulgnn0subcl  13546  mulgsubcl  13547  mhmmulg  13574  ghmmulg  13667  ringrghm  13899  dvdsrcl2  13936  crngunit  13948  dvdsrpropdg  13984  lss1d  14220  quscrng  14370  mulgghm2  14445  tgcl  14611  innei  14710  cncnp  14777  cnnei  14779  elbl2ps  14939  elbl2  14940  cncfco  15138  cnlimc  15219