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  5436  foco  5494  fun11iun  5528  fconstfvm  5783  isocnv  5861  f1oiso  5876  f1ocnvfv3  5914  tfrcl  6431  mapxpen  6918  findcard  6958  exmidfodomrlemim  7280  genpassl  7608  genpassu  7609  axsuploc  8116  cnegexlem3  8220  recexaplem2  8696  divap0  8728  dfinfre  9000  qreccl  9733  xrlttr  9887  addmodlteq  10507  cau3lem  11296  climcn1  11490  climcn2  11491  climcaucn  11533  ntrivcvgap  11730  rplpwr  12219  dvdssq  12223  nn0seqcvgd  12234  lcmgcdlem  12270  isprm6  12340  phiprmpw  12415  pcneg  12519  prmpwdvds  12549  4sqlem19  12603  grpinveu  13240  mulgnn0subcl  13341  mulgsubcl  13342  mhmmulg  13369  ghmmulg  13462  ringrghm  13694  dvdsrcl2  13731  crngunit  13743  dvdsrpropdg  13779  lss1d  14015  quscrng  14165  mulgghm2  14240  tgcl  14384  innei  14483  cncnp  14550  cnnei  14552  elbl2ps  14712  elbl2  14713  cncfco  14911  cnlimc  14992