Theorem an32s 574

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 568	. 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  577  anabss1  582  biadanid  622  fssres  5560  foco  5621  fun11iun  5655  fconstfvm  5924  isocnv  6007  f1oiso  6022  f1ocnvfv3  6064  tfrcl  6625  mapxpen  7138  findcard  7182  exmidfodomrlemim  7543  genpassl  7881  genpassu  7882  axsuploc  8388  cnegexlem3  8493  recexaplem2  8970  divap0  9004  dfinfre  9276  qreccl  10021  xrlttr  10176  addmodlteq  10813  cau3lem  11858  climcn1  12052  climcn2  12053  climcaucn  12095  ntrivcvgap  12293  rplpwr  12782  dvdssq  12786  nn0seqcvgd  12797  lcmgcdlem  12833  isprm6  12903  phiprmpw  12978  pcneg  13082  prmpwdvds  13112  4sqlem19  13166  grpinveu  13820  mulgnn0subcl  13915  mulgsubcl  13916  mhmmulg  13943  ghmmulg  14036  ringrghm  14340  dvdsrcl2  14379  crngunit  14391  dvdsrpropdg  14427  lss1d  14692  quscrng  14842  mulgghm2  14915  tgcl  15088  innei  15187  cncnp  15254  cnnei  15256  elbl2ps  15416  elbl2  15417  cncfco  15615  cnlimc  15696