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  5430  foco  5488  fun11iun  5522  fconstfvm  5777  isocnv  5855  f1oiso  5870  f1ocnvfv3  5908  tfrcl  6419  mapxpen  6906  findcard  6946  exmidfodomrlemim  7263  genpassl  7586  genpassu  7587  axsuploc  8094  cnegexlem3  8198  recexaplem2  8673  divap0  8705  dfinfre  8977  qreccl  9710  xrlttr  9864  addmodlteq  10472  cau3lem  11261  climcn1  11454  climcn2  11455  climcaucn  11497  ntrivcvgap  11694  rplpwr  12167  dvdssq  12171  nn0seqcvgd  12182  lcmgcdlem  12218  isprm6  12288  phiprmpw  12363  pcneg  12466  prmpwdvds  12496  4sqlem19  12550  grpinveu  13113  mulgnn0subcl  13208  mulgsubcl  13209  mhmmulg  13236  ghmmulg  13329  ringrghm  13561  dvdsrcl2  13598  crngunit  13610  dvdsrpropdg  13646  lss1d  13882  quscrng  14032  mulgghm2  14107  tgcl  14243  innei  14342  cncnp  14409  cnnei  14411  elbl2ps  14571  elbl2  14572  cncfco  14770  cnlimc  14851