Theorem an32s 779

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

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  anass1rs  782  anabss1  787  ncfinlower  4484  nnadjoin  4521  nnpweq  4524  tfinnn  4535  fssres  5239  foco  5280  f1ores  5301  fun11iun  5306  fconstfv  5457  isocnv  5492  isomin  5497  f1oiso  5500  ncssfin  6152  nntccl  6171  tlecg  6231  ce2le  6234  nnc3n3p1  6279  nchoicelem12  6301  nchoicelem19  6308