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  3557  inrab2  3574  reupick  3585  resco  5333  imadif  5487  f11o  5667  respreima  5818  dff1o6  5972  dfoprab2  6080  difxp  6339  xpassen  7161  dfac5lem1  7960  kmlem3  7988  qbtwnre  10741  elioomnf  10955  pcqcl  13185  tosso  14420  subgdmdprd  15547  opsrtoslem1  16499  pjfval2  16891  cmpcov2  17407  tx1cn  17594  tgphaus  18099  isms2  18433  elcncf1di  18878  elii1  18913  dvreslem  19749  dvdsflsumcom  20926  is2wlk  21518  cvnbtwn3  23744  1stmbfm  24563  ballotlem2  24699  dfon3  25646  brimg  25690  brsegle2  25947  bddiblnc  26174  prtlem17  26615  pm11.6  27459  stoweidlem17  27633  lcvnbtwn3  29511  cvrnbtwn3  29759  islpln5  30017  islvol5  30061  lhpexle3  30494  dibelval3  31630  dihglb2  31825
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