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

Theorem an32 796
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 649 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 795 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 450 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 271 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  an32s  802  3anan32  977  indifdir  3604  inrab2  3621  reupick  3632  difxp  5260  resco  5340  imadif  5491  respreima  5830  dff1o6  5980  dfoprab2  6131  f11o  6537  mpt2curryd  6786  xpassen  7403  dfac5lem1  8291  kmlem3  8319  qbtwnre  11167  elioomnf  11382  pcqcl  13921  tosso  15204  subgdmdprd  16529  opsrtoslem1  17563  pjfval2  18132  cmpcov2  18991  tx1cn  19180  tgphaus  19685  isms2  20023  elcncf1di  20469  elii1  20505  dvreslem  21382  dvdsflsumcom  22526  is2wlk  23462  cvnbtwn3  25690  ordtconlem1  26352  1stmbfm  26673  eulerpartlemn  26762  ballotlem2  26869  dfon3  27921  brsegle2  28138  bddiblnc  28459  ftc1anc  28472  prtlem17  29018  pm11.6  29642  stoweidlem17  29809  modfsummod  30242  lcvnbtwn3  32670  cvrnbtwn3  32918  islpln5  33176  islvol5  33220  lhpexle3  33653  dibelval3  34789  dihglb2  34984
  Copyright terms: Public domain W3C validator