MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an12 Unicode version

Theorem an12 773
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 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 677 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 631 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 267 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an32  774  an13  775  an12s  777  an4  798  ceqsrexv  3037  rmoan  3100  2reuswap  3104  reuind  3105  sbccomlem  3199  elunirab  3996  axsep  4297  reuxfr2d  4713  opeliunxp  4896  elres  5148  opabex3d  5956  opabex3  5957  resoprab  6133  ov6g  6178  oeeu  6813  xpassen  7169  omxpenlem  7176  dfac5lem2  7969  ltexprlem4  8880  rexuz2  10492  2clim  12329  divalglem10  12885  bitsmod  12911  isssc  13983  eldmcoa  14183  issubrg  15831  isbasis2g  16976  tgval2  16984  is1stc2  17466  elflim2  17957  i1fres  19558  dvdsflsumcom  20934  vmasum  20961  logfac2  20962  2reuswap2  23936  reuxfr3d  23937  1stpreima  24056  tfrALTlem  25498  nofulllem5  25582  brimg  25698  dfrdg4  25711  tfrqfree  25712  axcontlem2  25816  sstotbnd3  26383  2rmoswap  27837  bnj849  29014  islshpat  29512  islpln5  30029  islvol5  30073  cdleme0nex  30784  dicelval3  31675  mapdordlem1a  32129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator