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

Theorem an12 551
Description: Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
an12  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )

Proof of Theorem an12
StepHypRef Expression
1 ancom 264 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 454 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 399 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 399 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 209 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
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:  an32  552  an13  553  an12s  555  an4  576  ceqsrexv  2819  rmoan  2888  2reuswapdc  2892  reuind  2893  2rmorex  2894  sbccomlem  2987  elunirab  3757  rexxfrd  4392  opeliunxp  4602  elres  4863  resoprab  5875  ov6g  5916  opabex3d  6027  opabex3  6028  xpassen  6732  distrnqg  7219  distrnq0  7291  rexuz2  9403  2clim  11102  isbasis2g  12251  tgval2  12259
  Copyright terms: Public domain W3C validator