Theorem an32s 533

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  anass1rs  536  anabss1  541  fssres  5097  foco  5147  fun11iun  5178  fconstfvm  5411  isocnv  5482  f1oiso  5496  f1ocnvfv3  5532  tfrcl  6013  findcard  6422  genpassl  6776  genpassu  6777  cnegexlem3  7352  recexaplem2  7809  divap0  7839  dfinfre  8101  qreccl  8808  xrlttr  8946  addmodlteq  9480  cau3lem  10138  climcn1  10285  climcn2  10286  climcaucn  10326  rplpwr  10560  dvdssq  10564  nn0seqcvgd  10567  lcmgcdlem  10603  isprm6  10670