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  5453  foco  5511  fun11iun  5545  fconstfvm  5804  isocnv  5882  f1oiso  5897  f1ocnvfv3  5935  tfrcl  6452  mapxpen  6947  findcard  6987  exmidfodomrlemim  7311  genpassl  7639  genpassu  7640  axsuploc  8147  cnegexlem3  8251  recexaplem2  8727  divap0  8759  dfinfre  9031  qreccl  9765  xrlttr  9919  addmodlteq  10545  cau3lem  11458  climcn1  11652  climcn2  11653  climcaucn  11695  ntrivcvgap  11892  rplpwr  12381  dvdssq  12385  nn0seqcvgd  12396  lcmgcdlem  12432  isprm6  12502  phiprmpw  12577  pcneg  12681  prmpwdvds  12711  4sqlem19  12765  grpinveu  13403  mulgnn0subcl  13504  mulgsubcl  13505  mhmmulg  13532  ghmmulg  13625  ringrghm  13857  dvdsrcl2  13894  crngunit  13906  dvdsrpropdg  13942  lss1d  14178  quscrng  14328  mulgghm2  14403  tgcl  14569  innei  14668  cncnp  14735  cnnei  14737  elbl2ps  14897  elbl2  14898  cncfco  15096  cnlimc  15177