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

Theorem an12 773
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 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 677 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 631 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 267 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an32  774  an13  775  an12s  777  an4  798  ceqsrexv  3061  rmoan  3124  2reuswap  3128  reuind  3129  sbccomlem  3223  elunirab  4020  axsep  4321  reuxfr2d  4738  opeliunxp  4921  elres  5173  opabex3d  5981  opabex3  5982  resoprab  6158  ov6g  6203  oeeu  6838  xpassen  7194  omxpenlem  7201  dfac5lem2  7997  ltexprlem4  8908  rexuz2  10520  2clim  12358  divalglem10  12914  bitsmod  12940  isssc  14012  eldmcoa  14212  issubrg  15860  isbasis2g  17005  tgval2  17013  is1stc2  17497  elflim2  17988  i1fres  19589  dvdsflsumcom  20965  vmasum  20992  logfac2  20993  2reuswap2  23967  reuxfr3d  23968  1stpreima  24087  elima4  25396  nofulllem5  25653  elfuns  25752  brimg  25774  dfrdg4  25787  tfrqfree  25788  axcontlem2  25896  sstotbnd3  26466  2rmoswap  27919  bnj849  29223  islshpat  29742  islpln5  30259  islvol5  30303  cdleme0nex  31014  dicelval3  31905  mapdordlem1a  32359
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 178  df-an 361
  Copyright terms: Public domain W3C validator