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

Theorem an12 772
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 437 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 676 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 630 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 266 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  an32  773  an13  774  an12s  776  an4  797  ceqsrexv  2914  rmoan  2976  2reuswap  2980  reuind  2981  sbccomlem  3074  elunirab  3856  axsep  4156  reuxfr2d  4573  opeliunxp  4756  elres  5006  opabex3  5785  resoprab  5956  ov6g  6001  oeeu  6617  xpassen  6972  omxpenlem  6979  dfac5lem2  7767  ltexprlem4  8679  rexuz2  10286  2clim  12062  divalglem10  12617  bitsmod  12643  isssc  13713  eldmcoa  13913  issubrg  15561  isbasis2g  16702  tgval2  16710  is1stc2  17184  elflim2  17675  i1fres  19076  dvdsflsumcom  20444  vmasum  20471  logfac2  20472  2reuswap2  23153  reuxfr3d  23154  tfrALTlem  24347  nofulllem5  24431  brimg  24547  dfrdg4  24560  tfrqfree  24561  axcontlem2  24665  sstotbnd3  26603  2rmoswap  28065  opabex3d  28190  bnj849  29273  islshpat  29829  islpln5  30346  islvol5  30390  cdleme0nex  31101  dicelval3  31992  mapdordlem1a  32446
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 177  df-an 360
  Copyright terms: Public domain W3C validator