Theorem an32s 563

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 557	. 2 |- ( ( ( ph /\ ch ) /\ ps ) <-> ( ( ph /\ ps ) /\ ch ) )
2		an32s.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylbi 120	1 |- ( ( ( ph /\ ch ) /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anass1rs  566  anabss1  571  fssres  5373  foco  5430  fun11iun  5463  fconstfvm  5714  isocnv  5790  f1oiso  5805  f1ocnvfv3  5842  tfrcl  6343  mapxpen  6826  findcard  6866  exmidfodomrlemim  7178  genpassl  7486  genpassu  7487  axsuploc  7992  cnegexlem3  8096  recexaplem2  8570  divap0  8601  dfinfre  8872  qreccl  9601  xrlttr  9752  addmodlteq  10354  cau3lem  11078  climcn1  11271  climcn2  11272  climcaucn  11314  ntrivcvgap  11511  rplpwr  11982  dvdssq  11986  nn0seqcvgd  11995  lcmgcdlem  12031  isprm6  12101  phiprmpw  12176  pcneg  12278  prmpwdvds  12307  grpinveu  12741  tgcl  12858  innei  12957  cncnp  13024  cnnei  13026  elbl2ps  13186  elbl2  13187  cncfco  13372  cnlimc  13435