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  2852  2reuswap  2916  reuind  2917  sbccomlem  3005  elunirab  3781  axsep  4080  reuxfr2d  4494  opeliunxp  4693  elres  4943  opabex3  5668  resoprab  5839  ov6g  5884  oeeu  6534  xpassen  6889  omxpenlem  6896  dfac5lem2  7684  ltexprlem4  8596  rexuz2  10202  2clim  11976  divalglem10  12528  bitsmod  12554  isssc  13624  eldmcoa  13824  issubrg  15472  isbasis2g  16613  tgval2  16621  is1stc2  17095  elflim2  17586  i1fres  18987  dvdsflsumcom  20355  vmasum  20382  logfac2  20383  tfrALTlem  23610  brimg  23816  dfrdg4  23828  tfrqfree  23829  axcontlem2  23933  sstotbnd3  25832  bnj849  27969  islshpat  28337  islpln5  28854  islvol5  28898  cdleme0nex  29609  dicelval3  30500  mapdordlem1a  30954
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