Theorem an32s 574

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 568	. 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  577  anabss1  582  biadanid  622  fssres  5563  foco  5624  fun11iun  5658  fconstfvm  5927  isocnv  6010  f1oiso  6025  f1ocnvfv3  6067  tfrcl  6628  mapxpen  7141  findcard  7185  exmidfodomrlemim  7546  genpassl  7884  genpassu  7885  axsuploc  8391  cnegexlem3  8496  recexaplem2  8973  divap0  9007  dfinfre  9279  qreccl  10024  xrlttr  10179  addmodlteq  10816  cau3lem  11861  climcn1  12055  climcn2  12056  climcaucn  12098  ntrivcvgap  12296  rplpwr  12785  dvdssq  12789  nn0seqcvgd  12800  lcmgcdlem  12836  isprm6  12906  phiprmpw  12981  pcneg  13085  prmpwdvds  13115  4sqlem19  13169  grpinveu  13823  mulgnn0subcl  13918  mulgsubcl  13919  mhmmulg  13946  ghmmulg  14039  ringrghm  14343  dvdsrcl2  14382  crngunit  14394  dvdsrpropdg  14430  lss1d  14695  quscrng  14845  mulgghm2  14918  tgcl  15091  innei  15190  cncnp  15257  cnnei  15259  elbl2ps  15419  elbl2  15420  cncfco  15618  cnlimc  15699