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  3438  inrab2  3454  reupick  3465  resco  5193  imadif  5343  f11o  5522  respreima  5670  dff1o6  5807  dfoprab2  5911  difxp  6169  xpassen  6972  dfac5lem1  7766  kmlem3  7794  qbtwnre  10542  elioomnf  10754  pcqcl  12925  tosso  14158  subgdmdprd  15285  opsrtoslem1  16241  pjfval2  16625  cmpcov2  17133  tx1cn  17319  tgphaus  17815  isms2  18012  elcncf1di  18415  elii1  18449  dvreslem  19275  dvdsflsumcom  20444  cvnbtwn3  22884  1stmbfm  23580  dfon3  24503  brimg  24547  brsegle2  24804  bddiblnc  25021  prtlem17  26847  pm11.6  27694  stoweidlem17  27869  lcvnbtwn3  29840  cvrnbtwn3  30088  islpln5  30346  islvol5  30390  lhpexle3  30823  dibelval3  31959  dihglb2  32154
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