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  2869  rmoan  2931  2reuswap  2933  reuind  2934  sbccomlem  3022  elunirab  3800  axsep  4100  reuxfr2d  4515  opeliunxp  4714  elres  4964  opabex3  5689  resoprab  5860  ov6g  5905  oeeu  6555  xpassen  6910  omxpenlem  6917  dfac5lem2  7705  ltexprlem4  8617  rexuz2  10223  2clim  11997  divalglem10  12549  bitsmod  12575  isssc  13645  eldmcoa  13845  issubrg  15493  isbasis2g  16634  tgval2  16642  is1stc2  17116  elflim2  17607  i1fres  19008  dvdsflsumcom  20376  vmasum  20403  logfac2  20404  tfrALTlem  23631  brimg  23837  dfrdg4  23849  tfrqfree  23850  axcontlem2  23954  sstotbnd3  25853  bnj849  27990  islshpat  28358  islpln5  28875  islvol5  28919  cdleme0nex  29630  dicelval3  30521  mapdordlem1a  30975
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