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  fssres  5393  foco  5450  fun11iun  5484  fconstfvm  5736  isocnv  5814  f1oiso  5829  f1ocnvfv3  5866  tfrcl  6367  mapxpen  6850  findcard  6890  exmidfodomrlemim  7202  genpassl  7525  genpassu  7526  axsuploc  8032  cnegexlem3  8136  recexaplem2  8611  divap0  8643  dfinfre  8915  qreccl  9644  xrlttr  9797  addmodlteq  10400  cau3lem  11125  climcn1  11318  climcn2  11319  climcaucn  11361  ntrivcvgap  11558  rplpwr  12030  dvdssq  12034  nn0seqcvgd  12043  lcmgcdlem  12079  isprm6  12149  phiprmpw  12224  pcneg  12326  prmpwdvds  12355  grpinveu  12916  mulgnn0subcl  13001  mulgsubcl  13002  mhmmulg  13029  dvdsrcl2  13273  crngunit  13285  dvdsrpropdg  13321  lss1d  13475  tgcl  13603  innei  13702  cncnp  13769  cnnei  13771  elbl2ps  13931  elbl2  13932  cncfco  14117  cnlimc  14180