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

Theorem an12 528
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 262 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 446 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 393 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 393 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 208 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103
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:  an32  529  an13  530  an12s  532  an4  553  ceqsrexv  2747  rmoan  2815  2reuswapdc  2819  reuind  2820  2rmorex  2821  sbccomlem  2913  elunirab  3666  rexxfrd  4285  opeliunxp  4493  elres  4748  resoprab  5741  ov6g  5782  opabex3d  5892  opabex3  5893  xpassen  6546  distrnqg  6946  distrnq0  7018  rexuz2  9069  2clim  10689
  Copyright terms: Public domain W3C validator