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  614  fssres  5451  foco  5509  fun11iun  5543  fconstfvm  5802  isocnv  5880  f1oiso  5895  f1ocnvfv3  5933  tfrcl  6450  mapxpen  6945  findcard  6985  exmidfodomrlemim  7309  genpassl  7637  genpassu  7638  axsuploc  8145  cnegexlem3  8249  recexaplem2  8725  divap0  8757  dfinfre  9029  qreccl  9763  xrlttr  9917  addmodlteq  10543  cau3lem  11425  climcn1  11619  climcn2  11620  climcaucn  11662  ntrivcvgap  11859  rplpwr  12348  dvdssq  12352  nn0seqcvgd  12363  lcmgcdlem  12399  isprm6  12469  phiprmpw  12544  pcneg  12648  prmpwdvds  12678  4sqlem19  12732  grpinveu  13370  mulgnn0subcl  13471  mulgsubcl  13472  mhmmulg  13499  ghmmulg  13592  ringrghm  13824  dvdsrcl2  13861  crngunit  13873  dvdsrpropdg  13909  lss1d  14145  quscrng  14295  mulgghm2  14370  tgcl  14536  innei  14635  cncnp  14702  cnnei  14704  elbl2ps  14864  elbl2  14865  cncfco  15063  cnlimc  15144