Theorem an32s 557

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 551	. 2 |- ( ( ( ph /\ ch ) /\ ps ) <-> ( ( ph /\ ps ) /\ ch ) )
2		an32s.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylbi 120	1 |- ( ( ( ph /\ ch ) /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  anass1rs  560  anabss1  565  fssres  5298  foco  5355  fun11iun  5388  fconstfvm  5638  isocnv  5712  f1oiso  5727  f1ocnvfv3  5763  tfrcl  6261  mapxpen  6742  findcard  6782  exmidfodomrlemim  7057  genpassl  7332  genpassu  7333  axsuploc  7837  cnegexlem3  7939  recexaplem2  8413  divap0  8444  dfinfre  8714  qreccl  9434  xrlttr  9581  addmodlteq  10171  cau3lem  10886  climcn1  11077  climcn2  11078  climcaucn  11120  ntrivcvgap  11317  rplpwr  11715  dvdssq  11719  nn0seqcvgd  11722  lcmgcdlem  11758  isprm6  11825  phiprmpw  11898  tgcl  12233  innei  12332  cncnp  12399  cnnei  12401  elbl2ps  12561  elbl2  12562  cncfco  12747  cnlimc  12810