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  biadanid  616  fssres  5501  foco  5559  fun11iun  5593  fconstfvm  5857  isocnv  5935  f1oiso  5950  f1ocnvfv3  5990  tfrcl  6510  mapxpen  7009  findcard  7050  exmidfodomrlemim  7379  genpassl  7711  genpassu  7712  axsuploc  8219  cnegexlem3  8323  recexaplem2  8799  divap0  8831  dfinfre  9103  qreccl  9837  xrlttr  9991  addmodlteq  10620  cau3lem  11625  climcn1  11819  climcn2  11820  climcaucn  11862  ntrivcvgap  12059  rplpwr  12548  dvdssq  12552  nn0seqcvgd  12563  lcmgcdlem  12599  isprm6  12669  phiprmpw  12744  pcneg  12848  prmpwdvds  12878  4sqlem19  12932  grpinveu  13571  mulgnn0subcl  13672  mulgsubcl  13673  mhmmulg  13700  ghmmulg  13793  ringrghm  14025  dvdsrcl2  14063  crngunit  14075  dvdsrpropdg  14111  lss1d  14347  quscrng  14497  mulgghm2  14572  tgcl  14738  innei  14837  cncnp  14904  cnnei  14906  elbl2ps  15066  elbl2  15067  cncfco  15265  cnlimc  15346