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 450 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 695 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 649 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 649 . 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 369
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 371
This theorem is referenced by:  an32  796  an13  797  an12s  799  an4  822  ceqsrexv  3237  rmoan  3302  2reuswap  3306  reuind  3307  sbccomlem  3410  elunirab  4257  axsep  4567  reuxfr2d  4670  opeliunxp  5050  elres  5307  resoprab  6380  elrnmpt2res  6398  ov6g  6422  opabex3d  6759  opabex3  6760  oeeu  7249  xpassen  7608  omxpenlem  7615  dfac5lem2  8501  ltexprlem4  9413  rexuz2  11128  wrdeqswrdlsw  12633  2clim  13354  divalglem10  13915  bitsmod  13941  isssc  15046  eldmcoa  15246  issubrg  17212  isbasis2g  19216  tgval2  19224  is1stc2  19709  elflim2  20200  i1fres  21847  dvdsflsumcom  23192  vmasum  23219  logfac2  23220  axcontlem2  23944  2reuswap2  27063  reuxfr3d  27064  1stpreima  27196  elima4  28786  nofulllem5  29043  elfuns  29142  brimg  29164  dfrdg4  29177  tfrqfree  29178  sstotbnd3  29875  an12i  30101  selconj  30103  2rmoswap  31656  bnj849  33062  bj-axsep  33460  islshpat  33814  islpln5  34331  islvol5  34375  cdleme0nex  35086  dicelval3  35977  mapdordlem1a  36431
  Copyright terms: Public domain W3C validator