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

Theorem an32 774
Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
Assertion
Ref Expression
an32  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )

Proof of Theorem an32
StepHypRef Expression
1 anass 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 773 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 438 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 263 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an32s  780  3anan32  948  indifdir  3533  inrab2  3550  reupick  3561  resco  5307  imadif  5461  f11o  5641  respreima  5791  dff1o6  5945  dfoprab2  6053  difxp  6312  xpassen  7131  dfac5lem1  7930  kmlem3  7958  qbtwnre  10710  elioomnf  10924  pcqcl  13150  tosso  14385  subgdmdprd  15512  opsrtoslem1  16464  pjfval2  16852  cmpcov2  17368  tx1cn  17555  tgphaus  18060  isms2  18363  elcncf1di  18789  elii1  18824  dvreslem  19656  dvdsflsumcom  20833  cvnbtwn3  23632  1stmbfm  24397  ballotlem2  24518  dfon3  25449  brimg  25493  brsegle2  25750  bddiblnc  25968  prtlem17  26409  pm11.6  27253  stoweidlem17  27427  lcvnbtwn3  29194  cvrnbtwn3  29442  islpln5  29700  islvol5  29744  lhpexle3  30177  dibelval3  31313  dihglb2  31508
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