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

Theorem an32s 535
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 529 . 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  538  anabss1  543  fssres  5186  foco  5243  fun11iun  5274  fconstfvm  5515  isocnv  5590  f1oiso  5605  f1ocnvfv3  5641  tfrcl  6129  mapxpen  6562  findcard  6602  exmidfodomrlemim  6825  genpassl  7081  genpassu  7082  cnegexlem3  7657  recexaplem2  8119  divap0  8149  dfinfre  8415  qreccl  9125  xrlttr  9263  addmodlteq  9801  cau3lem  10543  climcn1  10693  climcn2  10694  climcaucn  10736  rplpwr  11290  dvdssq  11294  nn0seqcvgd  11297  lcmgcdlem  11333  isprm6  11400  phiprmpw  11472  cncfco  11602
  Copyright terms: Public domain W3C validator