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

Theorem an32 536
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 398 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 535 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 264 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 205 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
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:  an32s  542  3anan32  958  indifdir  3302  inrab2  3319  reupick  3330  unidif0  4061  resco  5013  f11o  5368  respreima  5516  dff1o6  5645  dfoprab2  5786  xpassen  6692  enq0enq  7207  elioomnf  9719  modfsummod  11195  tx1cn  12365  isms2  12550  elcncf1di  12662
  Copyright terms: Public domain W3C validator