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

Theorem an12 806
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 452 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 701 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 655 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 655 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 279 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  an32  807  an13  808  an12s  810  an4  833  ceqsrexv  3172  rmoan  3238  2reuswap  3242  reuind  3243  sbccomlem  3338  elunirab  4210  axsep  4524  reuxfr2d  4623  opeliunxp  4886  elres  5140  resoprab  6392  elrnmpt2res  6410  ov6g  6434  opabex3d  6771  opabex3  6772  dfrecs3  7091  oeeu  7304  xpassen  7666  omxpenlem  7673  dfac5lem2  8555  ltexprlem4  9464  rexuz2  11210  2clim  13636  divalglem10  14383  bitsmod  14410  isssc  15725  eldmcoa  15960  issubrg  18008  isbasis2g  19963  tgval2  19971  is1stc2  20457  elflim2  20979  i1fres  22663  dvdsflsumcom  24117  vmasum  24144  logfac2  24145  axcontlem2  24995  2reuswap2  28124  reuxfr3d  28125  1stpreima  28287  bnj849  29736  elima4  30421  nofulllem5  30595  elfuns  30682  brimg  30704  dfrecs2  30717  dfrdg4  30718  bj-axsep  31408  mptsnunlem  31740  relowlpssretop  31767  poimirlem27  31967  sstotbnd3  32108  an12i  32334  selconj  32336  islshpat  32583  islpln5  33100  islvol5  33144  cdleme0nex  33856  dicelval3  34748  mapdordlem1a  35202  2rmoswap  38605
  Copyright terms: Public domain W3C validator