Theorem an32s 558

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 552	. 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  561  anabss1  566  fssres  5362  foco  5419  fun11iun  5452  fconstfvm  5702  isocnv  5778  f1oiso  5793  f1ocnvfv3  5830  tfrcl  6328  mapxpen  6810  findcard  6850  exmidfodomrlemim  7153  genpassl  7461  genpassu  7462  axsuploc  7967  cnegexlem3  8071  recexaplem2  8545  divap0  8576  dfinfre  8847  qreccl  9576  xrlttr  9727  addmodlteq  10329  cau3lem  11052  climcn1  11245  climcn2  11246  climcaucn  11288  ntrivcvgap  11485  rplpwr  11956  dvdssq  11960  nn0seqcvgd  11969  lcmgcdlem  12005  isprm6  12075  phiprmpw  12150  pcneg  12252  prmpwdvds  12281  tgcl  12664  innei  12763  cncnp  12830  cnnei  12832  elbl2ps  12992  elbl2  12993  cncfco  13178  cnlimc  13241