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

Theorem an12 774
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 678 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 632 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 632 . 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  775  an13  776  an12s  778  an4  799  ceqsrexv  2902  rmoan  2964  2reuswap  2968  reuind  2969  sbccomlem  3062  elunirab  3841  axsep  4141  reuxfr2d  4556  opeliunxp  4739  elres  4989  opabex3  5730  resoprab  5901  ov6g  5946  oeeu  6596  xpassen  6951  omxpenlem  6958  dfac5lem2  7746  ltexprlem4  8658  rexuz2  10265  2clim  12040  divalglem10  12595  bitsmod  12621  isssc  13691  eldmcoa  13891  issubrg  15539  isbasis2g  16680  tgval2  16688  is1stc2  17162  elflim2  17653  i1fres  19054  dvdsflsumcom  20422  vmasum  20449  logfac2  20450  tfrALTlem  23677  brimg  23883  dfrdg4  23895  tfrqfree  23896  axcontlem2  24000  sstotbnd3  25899  2rmoswap  27341  bnj849  28224  islshpat  28474  islpln5  28991  islvol5  29035  cdleme0nex  29746  dicelval3  30637  mapdordlem1a  31091
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