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  5571  fun11iun  5605  fconstfvm  5873  isocnv  5955  f1oiso  5970  f1ocnvfv3  6010  tfrcl  6533  mapxpen  7037  findcard  7080  exmidfodomrlemim  7415  genpassl  7747  genpassu  7748  axsuploc  8255  cnegexlem3  8359  recexaplem2  8835  divap0  8867  dfinfre  9139  qreccl  9879  xrlttr  10033  addmodlteq  10664  cau3lem  11695  climcn1  11889  climcn2  11890  climcaucn  11932  ntrivcvgap  12130  rplpwr  12619  dvdssq  12623  nn0seqcvgd  12634  lcmgcdlem  12670  isprm6  12740  phiprmpw  12815  pcneg  12919  prmpwdvds  12949  4sqlem19  13003  grpinveu  13642  mulgnn0subcl  13743  mulgsubcl  13744  mhmmulg  13771  ghmmulg  13864  ringrghm  14097  dvdsrcl2  14135  crngunit  14147  dvdsrpropdg  14183  lss1d  14419  quscrng  14569  mulgghm2  14644  tgcl  14815  innei  14914  cncnp  14981  cnnei  14983  elbl2ps  15143  elbl2  15144  cncfco  15342  cnlimc  15423