Theorem an32s 570

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 564	. 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  573  anabss1  578  biadanid  618  fssres  5512  foco  5570  fun11iun  5604  fconstfvm  5872  isocnv  5952  f1oiso  5967  f1ocnvfv3  6007  tfrcl  6530  mapxpen  7034  findcard  7077  exmidfodomrlemim  7412  genpassl  7744  genpassu  7745  axsuploc  8252  cnegexlem3  8356  recexaplem2  8832  divap0  8864  dfinfre  9136  qreccl  9876  xrlttr  10030  addmodlteq  10660  cau3lem  11675  climcn1  11869  climcn2  11870  climcaucn  11912  ntrivcvgap  12110  rplpwr  12599  dvdssq  12603  nn0seqcvgd  12614  lcmgcdlem  12650  isprm6  12720  phiprmpw  12795  pcneg  12899  prmpwdvds  12929  4sqlem19  12983  grpinveu  13622  mulgnn0subcl  13723  mulgsubcl  13724  mhmmulg  13751  ghmmulg  13844  ringrghm  14077  dvdsrcl2  14115  crngunit  14127  dvdsrpropdg  14163  lss1d  14399  quscrng  14549  mulgghm2  14624  tgcl  14790  innei  14889  cncnp  14956  cnnei  14958  elbl2ps  15118  elbl2  15119  cncfco  15317  cnlimc  15398