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

Theorem an12 795
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 448 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 693 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 647 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 647 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 275 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  an32  796  an13  797  an12s  799  an4  822  ceqsrexv  3171  rmoan  3236  2reuswap  3240  reuind  3241  sbccomlem  3336  elunirab  4188  axsep  4500  reuxfr2d  4598  opeliunxp  4978  elres  5234  resoprab  6315  elrnmpt2res  6333  ov6g  6357  opabex3d  6695  opabex3  6696  oeeu  7188  xpassen  7548  omxpenlem  7555  dfac5lem2  8436  ltexprlem4  9346  rexuz2  11070  2clim  13416  divalglem10  14081  bitsmod  14107  isssc  15245  eldmcoa  15480  issubrg  17561  isbasis2g  19553  tgval2  19561  is1stc2  20047  elflim2  20569  i1fres  22216  dvdsflsumcom  23600  vmasum  23627  logfac2  23628  axcontlem2  24410  2reuswap2  27527  reuxfr3d  27528  1stpreima  27702  elima4  29410  nofulllem5  29667  elfuns  29754  brimg  29776  dfrdg4  29789  tfrqfree  29790  sstotbnd3  30474  an12i  30700  selconj  30702  2rmoswap  32390  bnj849  34365  bj-axsep  34761  islshpat  35190  islpln5  35707  islvol5  35751  cdleme0nex  36463  dicelval3  37355  mapdordlem1a  37809
  Copyright terms: Public domain W3C validator