Theorem an32s 574

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 568	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anass1rs  577  anabss1  582  biadanid  622  fssres  5568  foco  5629  fun11iun  5663  fconstfvm  5936  isocnv  6020  f1oiso  6035  f1ocnvfv3  6077  tfrcl  6640  mapxpen  7154  findcard  7198  exmidfodomrlemim  7559  genpassl  7897  genpassu  7898  axsuploc  8404  cnegexlem3  8510  recexaplem2  8988  divap0  9022  dfinfre  9294  qreccl  10057  xrlttr  10213  addmodlteq  10855  cau3lem  11902  climcn1  12098  climcn2  12099  climcaucn  12141  ntrivcvgap  12339  rplpwr  12828  dvdssq  12832  nn0seqcvgd  12843  lcmgcdlem  12879  isprm6  12950  phiprmpw  13028  pcneg  13132  prmpwdvds  13162  4sqlem19  13216  grpinveu  13901  mulgnn0subcl  13996  mulgsubcl  13997  mhmmulg  14024  ghmmulg  14117  ringrghm  14473  dvdsrcl2  14514  crngunit  14526  dvdsrpropdg  14562  lss1d  14828  quscrng  14978  mulgghm2  15051  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  tgcl  15307  innei  15406  cncnp  15473  cnnei  15475  elbl2ps  15635  elbl2  15636  cncfco  15834  cnlimc  15915  logdivlt  16141