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

Theorem an32 562
Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
Assertion
Ref Expression
an32  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )

Proof of Theorem an32
StepHypRef Expression
1 anass 401 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 561 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 266 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 206 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105
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:  an32s  568  3anan32  990  indifdir  3405  inrab2  3422  reupick  3433  unidif0  4181  resco  5147  f11o  5508  respreima  5659  dff1o6  5792  dfoprab2  5937  xpassen  6847  enq0enq  7447  elioomnf  9985  modfsummod  11483  pcqcl  12323  tx1cn  14152  isms2  14337  elcncf1di  14449
  Copyright terms: Public domain W3C validator