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  6639  mapxpen  7152  findcard  7196  exmidfodomrlemim  7559  genpassl  7897  genpassu  7898  axsuploc  8404  cnegexlem3  8510  recexaplem2  8988  divap0  9022  dfinfre  9294  qreccl  10058  xrlttr  10214  addmodlteq  10856  cau3lem  11903  climcn1  12099  climcn2  12100  climcaucn  12142  ntrivcvgap  12340  rplpwr  12829  dvdssq  12833  nn0seqcvgd  12844  lcmgcdlem  12880  isprm6  12951  phiprmpw  13029  pcneg  13133  prmpwdvds  13163  4sqlem19  13217  grpinveu  13902  mulgnn0subcl  13997  mulgsubcl  13998  mhmmulg  14025  ghmmulg  14118  ringrghm  14474  dvdsrcl2  14515  crngunit  14527  dvdsrpropdg  14563  lss1d  14829  quscrng  14979  mulgghm2  15052  tgcl  15290  innei  15389  cncnp  15456  cnnei  15458  elbl2ps  15618  elbl2  15619  cncfco  15817  cnlimc  15898  logdivlt  16124