ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  an32s Unicode version

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
StepHypRef Expression
1 an32 527 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 119 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator