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

Theorem an12 805
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 452 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 700 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 654 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 654 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 279 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  an32  806  an13  807  an12s  809  an4  832  ceqsrexv  3206  rmoan  3271  2reuswap  3275  reuind  3276  sbccomlem  3371  elunirab  4229  axsep  4543  reuxfr2d  4642  opeliunxp  4903  elres  5157  resoprab  6404  elrnmpt2res  6422  ov6g  6446  opabex3d  6783  opabex3  6784  dfrecs3  7097  oeeu  7310  xpassen  7670  omxpenlem  7677  dfac5lem2  8557  ltexprlem4  9466  rexuz2  11212  2clim  13629  divalglem10  14376  bitsmod  14403  isssc  15718  eldmcoa  15953  issubrg  18001  isbasis2g  19955  tgval2  19963  is1stc2  20449  elflim2  20971  i1fres  22655  dvdsflsumcom  24109  vmasum  24136  logfac2  24137  axcontlem2  24987  2reuswap2  28116  reuxfr3d  28117  1stpreima  28283  bnj849  29738  elima4  30422  nofulllem5  30594  elfuns  30681  brimg  30703  dfrecs2  30716  dfrdg4  30717  bj-axsep  31372  mptsnunlem  31698  relowlpssretop  31725  poimirlem27  31925  sstotbnd3  32066  an12i  32292  selconj  32294  islshpat  32546  islpln5  33063  islvol5  33107  cdleme0nex  33819  dicelval3  34711  mapdordlem1a  35165  2rmoswap  38362
  Copyright terms: Public domain W3C validator