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

Theorem an12 773
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 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 677 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 anass 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
4 anass 631 . 2  |-  ( ( ( ps  /\  ph )  /\  ch )  <->  ( ps  /\  ( ph  /\  ch ) ) )
52, 3, 43bitr3i 267 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an32  774  an13  775  an12s  777  an4  798  ceqsrexv  3029  rmoan  3092  2reuswap  3096  reuind  3097  sbccomlem  3191  elunirab  3988  axsep  4289  reuxfr2d  4705  opeliunxp  4888  elres  5140  opabex3d  5948  opabex3  5949  resoprab  6125  ov6g  6170  oeeu  6805  xpassen  7161  omxpenlem  7168  dfac5lem2  7961  ltexprlem4  8872  rexuz2  10484  2clim  12321  divalglem10  12877  bitsmod  12903  isssc  13975  eldmcoa  14175  issubrg  15823  isbasis2g  16968  tgval2  16976  is1stc2  17458  elflim2  17949  i1fres  19550  dvdsflsumcom  20926  vmasum  20953  logfac2  20954  2reuswap2  23928  reuxfr3d  23929  1stpreima  24048  tfrALTlem  25490  nofulllem5  25574  brimg  25690  dfrdg4  25703  tfrqfree  25704  axcontlem2  25808  sstotbnd3  26375  2rmoswap  27829  bnj849  29002  islshpat  29500  islpln5  30017  islvol5  30061  cdleme0nex  30772  dicelval3  31663  mapdordlem1a  32117
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 178  df-an 361
  Copyright terms: Public domain W3C validator