Theorem an32s 570

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 564	. 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  573  anabss1  578  biadanid  618  fssres  5542  foco  5603  fun11iun  5637  fconstfvm  5904  isocnv  5986  f1oiso  6001  f1ocnvfv3  6041  tfrcl  6597  mapxpen  7103  findcard  7147  exmidfodomrlemim  7506  genpassl  7841  genpassu  7842  axsuploc  8348  cnegexlem3  8452  recexaplem2  8928  divap0  8960  dfinfre  9232  qreccl  9977  xrlttr  10131  addmodlteq  10764  cau3lem  11803  climcn1  11997  climcn2  11998  climcaucn  12040  ntrivcvgap  12238  rplpwr  12727  dvdssq  12731  nn0seqcvgd  12742  lcmgcdlem  12778  isprm6  12848  phiprmpw  12923  pcneg  13027  prmpwdvds  13057  4sqlem19  13111  grpinveu  13768  mulgnn0subcl  13869  mulgsubcl  13870  mhmmulg  13897  ghmmulg  13990  ringrghm  14223  dvdsrcl2  14261  crngunit  14273  dvdsrpropdg  14309  lss1d  14548  quscrng  14698  mulgghm2  14773  tgcl  14946  innei  15045  cncnp  15112  cnnei  15114  elbl2ps  15274  elbl2  15275  cncfco  15473  cnlimc  15554