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  5403  foco  5460  fun11iun  5494  fconstfvm  5747  isocnv  5825  f1oiso  5840  f1ocnvfv3  5877  tfrcl  6379  mapxpen  6862  findcard  6902  exmidfodomrlemim  7214  genpassl  7537  genpassu  7538  axsuploc  8044  cnegexlem3  8148  recexaplem2  8623  divap0  8655  dfinfre  8927  qreccl  9656  xrlttr  9809  addmodlteq  10412  cau3lem  11137  climcn1  11330  climcn2  11331  climcaucn  11373  ntrivcvgap  11570  rplpwr  12042  dvdssq  12046  nn0seqcvgd  12055  lcmgcdlem  12091  isprm6  12161  phiprmpw  12236  pcneg  12338  prmpwdvds  12367  grpinveu  12943  mulgnn0subcl  13036  mulgsubcl  13037  mhmmulg  13064  ghmmulg  13150  dvdsrcl2  13404  crngunit  13416  dvdsrpropdg  13452  lss1d  13629  quscrng  13777  tgcl  13917  innei  14016  cncnp  14083  cnnei  14085  elbl2ps  14245  elbl2  14246  cncfco  14431  cnlimc  14494