Theorem an32s 574

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 568	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anass1rs  577  anabss1  582  biadanid  622  fssres  5565  foco  5626  fun11iun  5660  fconstfvm  5933  isocnv  6017  f1oiso  6032  f1ocnvfv3  6074  tfrcl  6635  mapxpen  7148  findcard  7192  exmidfodomrlemim  7553  genpassl  7891  genpassu  7892  axsuploc  8398  cnegexlem3  8503  recexaplem2  8980  divap0  9014  dfinfre  9286  qreccl  10042  xrlttr  10197  addmodlteq  10835  cau3lem  11880  climcn1  12074  climcn2  12075  climcaucn  12117  ntrivcvgap  12315  rplpwr  12804  dvdssq  12808  nn0seqcvgd  12819  lcmgcdlem  12855  isprm6  12925  phiprmpw  13000  pcneg  13104  prmpwdvds  13134  4sqlem19  13188  grpinveu  13843  mulgnn0subcl  13938  mulgsubcl  13939  mhmmulg  13966  ghmmulg  14059  ringrghm  14367  dvdsrcl2  14406  crngunit  14418  dvdsrpropdg  14454  lss1d  14720  quscrng  14870  mulgghm2  14943  tgcl  15165  innei  15264  cncnp  15331  cnnei  15333  elbl2ps  15493  elbl2  15494  cncfco  15692  cnlimc  15773