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  fssres  5392  foco  5449  fun11iun  5483  fconstfvm  5735  isocnv  5812  f1oiso  5827  f1ocnvfv3  5864  tfrcl  6365  mapxpen  6848  findcard  6888  exmidfodomrlemim  7200  genpassl  7523  genpassu  7524  axsuploc  8030  cnegexlem3  8134  recexaplem2  8609  divap0  8641  dfinfre  8913  qreccl  9642  xrlttr  9795  addmodlteq  10398  cau3lem  11123  climcn1  11316  climcn2  11317  climcaucn  11359  ntrivcvgap  11556  rplpwr  12028  dvdssq  12032  nn0seqcvgd  12041  lcmgcdlem  12077  isprm6  12147  phiprmpw  12222  pcneg  12324  prmpwdvds  12353  grpinveu  12911  mulgnn0subcl  12996  mulgsubcl  12997  mhmmulg  13024  dvdsrcl2  13268  crngunit  13280  dvdsrpropdg  13316  tgcl  13567  innei  13666  cncnp  13733  cnnei  13735  elbl2ps  13895  elbl2  13896  cncfco  14081  cnlimc  14144