Theorem an32s 502

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  anass1rs  505  anabss1  510  fssres  5066  foco  5116  fun11iun  5147  fconstfvm  5379  isocnv  5451  f1oiso  5465  f1ocnvfv3  5501  findcard  6345  genpassl  6622  genpassu  6623  cnegexlem3  7188  recexaplem2  7633  divap0  7663  qreccl  8576  xrlttr  8716  cau3lem  9710  climcn1  9829  climcn2  9830  climcaucn  9870  nn0seqcvgd  9880