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

Theorem an12 775
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 439 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 679 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 633 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 633 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 268 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  an32  776  an13  777  an12s  779  an4  800  ceqsrexv  2838  2reuswap  2902  reuind  2903  sbccomlem  2991  elunirab  3740  axsep  4037  reuxfr2d  4448  opeliunxp  4647  elres  4897  opabex3  5621  resoprab  5792  ov6g  5837  oeeu  6487  xpassen  6841  omxpenlem  6848  dfac5lem2  7635  ltexprlem4  8543  rexuz2  10149  2clim  11923  divalglem10  12475  bitsmod  12501  isssc  13541  eldmcoa  13741  issubrg  15380  isbasis2g  16518  tgval2  16526  is1stc2  17000  elflim2  17491  i1fres  18892  dvdsflsumcom  20260  vmasum  20287  logfac2  20288  tfrALTlem  23444  brimg  23650  dfrdg4  23662  tfrqfree  23663  axcontlem2  23767  sstotbnd3  25666  bnj849  27646  islshpat  27896  islpln5  28413  islvol5  28457  cdleme0nex  29168  dicelval3  30059  mapdordlem1a  30513
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator