Theorem an32s 568

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anass1rs  571  anabss1  576  biadanid  614  fssres  5433  foco  5491  fun11iun  5525  fconstfvm  5780  isocnv  5858  f1oiso  5873  f1ocnvfv3  5911  tfrcl  6422  mapxpen  6909  findcard  6949  exmidfodomrlemim  7268  genpassl  7591  genpassu  7592  axsuploc  8099  cnegexlem3  8203  recexaplem2  8679  divap0  8711  dfinfre  8983  qreccl  9716  xrlttr  9870  addmodlteq  10490  cau3lem  11279  climcn1  11473  climcn2  11474  climcaucn  11516  ntrivcvgap  11713  rplpwr  12194  dvdssq  12198  nn0seqcvgd  12209  lcmgcdlem  12245  isprm6  12315  phiprmpw  12390  pcneg  12494  prmpwdvds  12524  4sqlem19  12578  grpinveu  13170  mulgnn0subcl  13265  mulgsubcl  13266  mhmmulg  13293  ghmmulg  13386  ringrghm  13618  dvdsrcl2  13655  crngunit  13667  dvdsrpropdg  13703  lss1d  13939  quscrng  14089  mulgghm2  14164  tgcl  14300  innei  14399  cncnp  14466  cnnei  14468  elbl2ps  14628  elbl2  14629  cncfco  14827  cnlimc  14908