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

Theorem an32s 557
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 551 . 2  |-  ( ( ( ph  /\  ch )  /\  ps )  <->  ( ( ph  /\  ps )  /\  ch ) )
2 an32s.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylbi 120 1  |-  ( ( ( ph  /\  ch )  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  anass1rs  560  anabss1  565  fssres  5293  foco  5350  fun11iun  5381  fconstfvm  5631  isocnv  5705  f1oiso  5720  f1ocnvfv3  5756  tfrcl  6254  mapxpen  6735  findcard  6775  exmidfodomrlemim  7050  genpassl  7325  genpassu  7326  axsuploc  7830  cnegexlem3  7932  recexaplem2  8406  divap0  8437  dfinfre  8707  qreccl  9427  xrlttr  9574  addmodlteq  10164  cau3lem  10879  climcn1  11070  climcn2  11071  climcaucn  11113  ntrivcvgap  11310  rplpwr  11704  dvdssq  11708  nn0seqcvgd  11711  lcmgcdlem  11747  isprm6  11814  phiprmpw  11887  tgcl  12222  innei  12321  cncnp  12388  cnnei  12390  elbl2ps  12550  elbl2  12551  cncfco  12736  cnlimc  12799
  Copyright terms: Public domain W3C validator