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

Theorem an32 773
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 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 772 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 437 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 262 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  an32s  779  3anan32  946  indifdir  3425  inrab2  3441  reupick  3452  resco  5177  imadif  5327  f11o  5506  respreima  5654  dff1o6  5791  dfoprab2  5895  difxp  6153  xpassen  6956  dfac5lem1  7750  kmlem3  7778  qbtwnre  10526  elioomnf  10738  pcqcl  12909  tosso  14142  subgdmdprd  15269  opsrtoslem1  16225  pjfval2  16609  cmpcov2  17117  tx1cn  17303  tgphaus  17799  isms2  17996  elcncf1di  18399  elii1  18433  dvreslem  19259  dvdsflsumcom  20428  cvnbtwn3  22868  1stmbfm  23565  dfon3  24432  brimg  24476  brsegle2  24732  prtlem17  26744  pm11.6  27591  stoweidlem17  27766  lcvnbtwn3  29218  cvrnbtwn3  29466  islpln5  29724  islvol5  29768  lhpexle3  30201  dibelval3  31337  dihglb2  31532
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 177  df-an 360
  Copyright terms: Public domain W3C validator