Theorem an32s 568

Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)

Hypothesis

Ref	Expression
an32s.1	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
an32s	|- ( ( ( ph /\ ch ) /\ ps ) -> th )

Proof of Theorem an32s

Step	Hyp	Ref	Expression
1		an32 562	. 2 |- ( ( ( ph /\ ch ) /\ ps ) <-> ( ( ph /\ ps ) /\ ch ) )
2		an32s.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylbi 121	1 |- ( ( ( ph /\ ch ) /\ ps ) -> th )

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  5473  foco  5531  fun11iun  5565  fconstfvm  5825  isocnv  5903  f1oiso  5918  f1ocnvfv3  5956  tfrcl  6473  mapxpen  6970  findcard  7011  exmidfodomrlemim  7340  genpassl  7672  genpassu  7673  axsuploc  8180  cnegexlem3  8284  recexaplem2  8760  divap0  8792  dfinfre  9064  qreccl  9798  xrlttr  9952  addmodlteq  10580  cau3lem  11540  climcn1  11734  climcn2  11735  climcaucn  11777  ntrivcvgap  11974  rplpwr  12463  dvdssq  12467  nn0seqcvgd  12478  lcmgcdlem  12514  isprm6  12584  phiprmpw  12659  pcneg  12763  prmpwdvds  12793  4sqlem19  12847  grpinveu  13485  mulgnn0subcl  13586  mulgsubcl  13587  mhmmulg  13614  ghmmulg  13707  ringrghm  13939  dvdsrcl2  13976  crngunit  13988  dvdsrpropdg  14024  lss1d  14260  quscrng  14410  mulgghm2  14485  tgcl  14651  innei  14750  cncnp  14817  cnnei  14819  elbl2ps  14979  elbl2  14980  cncfco  15178  cnlimc  15259