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  5565  foco  5626  fun11iun  5660  fconstfvm  5933  isocnv  6017  f1oiso  6032  f1ocnvfv3  6074  tfrcl  6635  mapxpen  7148  findcard  7192  exmidfodomrlemim  7554  genpassl  7892  genpassu  7893  axsuploc  8399  cnegexlem3  8505  recexaplem2  8983  divap0  9017  dfinfre  9289  qreccl  10052  xrlttr  10208  addmodlteq  10850  cau3lem  11897  climcn1  12093  climcn2  12094  climcaucn  12136  ntrivcvgap  12334  rplpwr  12823  dvdssq  12827  nn0seqcvgd  12838  lcmgcdlem  12874  isprm6  12945  phiprmpw  13023  pcneg  13127  prmpwdvds  13157  4sqlem19  13211  grpinveu  13896  mulgnn0subcl  13991  mulgsubcl  13992  mhmmulg  14019  ghmmulg  14112  ringrghm  14451  dvdsrcl2  14490  crngunit  14502  dvdsrpropdg  14538  lss1d  14804  quscrng  14954  mulgghm2  15027  tgcl  15256  innei  15355  cncnp  15422  cnnei  15424  elbl2ps  15584  elbl2  15585  cncfco  15783  cnlimc  15864  logdivlt  16088