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

Theorem an12 772
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 437 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 676 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 630 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 266 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  an32  773  an13  774  an12s  776  an4  797  ceqsrexv  2901  rmoan  2963  2reuswap  2967  reuind  2968  sbccomlem  3061  elunirab  3840  axsep  4140  reuxfr2d  4557  opeliunxp  4740  elres  4990  opabex3  5769  resoprab  5940  ov6g  5985  oeeu  6601  xpassen  6956  omxpenlem  6963  dfac5lem2  7751  ltexprlem4  8663  rexuz2  10270  2clim  12046  divalglem10  12601  bitsmod  12627  isssc  13697  eldmcoa  13897  issubrg  15545  isbasis2g  16686  tgval2  16694  is1stc2  17168  elflim2  17659  i1fres  19060  dvdsflsumcom  20428  vmasum  20455  logfac2  20456  2reuswap2  23137  reuxfr3d  23138  tfrALTlem  24276  nofulllem5  24360  brimg  24476  dfrdg4  24488  tfrqfree  24489  axcontlem2  24593  sstotbnd3  26500  2rmoswap  27962  bnj849  28957  islshpat  29207  islpln5  29724  islvol5  29768  cdleme0nex  30479  dicelval3  31370  mapdordlem1a  31824
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 177  df-an 360
  Copyright terms: Public domain W3C validator