MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  an12 Structured version   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  3069  rmoan  3132  2reuswap  3136  reuind  3137  sbccomlem  3231  elunirab  4028  axsep  4329  reuxfr2d  4746  opeliunxp  4929  elres  5181  opabex3d  5989  opabex3  5990  resoprab  6166  ov6g  6211  oeeu  6846  xpassen  7202  omxpenlem  7209  dfac5lem2  8005  ltexprlem4  8916  rexuz2  10528  2clim  12366  divalglem10  12922  bitsmod  12948  isssc  14020  eldmcoa  14220  issubrg  15868  isbasis2g  17013  tgval2  17021  is1stc2  17505  elflim2  17996  i1fres  19597  dvdsflsumcom  20973  vmasum  21000  logfac2  21001  2reuswap2  23975  reuxfr3d  23976  1stpreima  24095  elima4  25404  nofulllem5  25661  elfuns  25760  brimg  25782  dfrdg4  25795  tfrqfree  25796  axcontlem2  25904  sstotbnd3  26485  2rmoswap  27938  bnj849  29296  islshpat  29815  islpln5  30332  islvol5  30376  cdleme0nex  31087  dicelval3  31978  mapdordlem1a  32432
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