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  5429  foco  5487  fun11iun  5521  fconstfvm  5776  isocnv  5854  f1oiso  5869  f1ocnvfv3  5907  tfrcl  6417  mapxpen  6904  findcard  6944  exmidfodomrlemim  7261  genpassl  7584  genpassu  7585  axsuploc  8092  cnegexlem3  8196  recexaplem2  8671  divap0  8703  dfinfre  8975  qreccl  9707  xrlttr  9861  addmodlteq  10469  cau3lem  11258  climcn1  11451  climcn2  11452  climcaucn  11494  ntrivcvgap  11691  rplpwr  12164  dvdssq  12168  nn0seqcvgd  12179  lcmgcdlem  12215  isprm6  12285  phiprmpw  12360  pcneg  12463  prmpwdvds  12493  4sqlem19  12547  grpinveu  13110  mulgnn0subcl  13205  mulgsubcl  13206  mhmmulg  13233  ghmmulg  13326  ringrghm  13558  dvdsrcl2  13595  crngunit  13607  dvdsrpropdg  13643  lss1d  13879  quscrng  14029  mulgghm2  14096  tgcl  14232  innei  14331  cncnp  14398  cnnei  14400  elbl2ps  14560  elbl2  14561  cncfco  14746  cnlimc  14826