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  616  fssres  5503  foco  5561  fun11iun  5595  fconstfvm  5861  isocnv  5941  f1oiso  5956  f1ocnvfv3  5996  tfrcl  6516  mapxpen  7017  findcard  7058  exmidfodomrlemim  7390  genpassl  7722  genpassu  7723  axsuploc  8230  cnegexlem3  8334  recexaplem2  8810  divap0  8842  dfinfre  9114  qreccl  9849  xrlttr  10003  addmodlteq  10632  cau3lem  11641  climcn1  11835  climcn2  11836  climcaucn  11878  ntrivcvgap  12075  rplpwr  12564  dvdssq  12568  nn0seqcvgd  12579  lcmgcdlem  12615  isprm6  12685  phiprmpw  12760  pcneg  12864  prmpwdvds  12894  4sqlem19  12948  grpinveu  13587  mulgnn0subcl  13688  mulgsubcl  13689  mhmmulg  13716  ghmmulg  13809  ringrghm  14041  dvdsrcl2  14079  crngunit  14091  dvdsrpropdg  14127  lss1d  14363  quscrng  14513  mulgghm2  14588  tgcl  14754  innei  14853  cncnp  14920  cnnei  14922  elbl2ps  15082  elbl2  15083  cncfco  15281  cnlimc  15362