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

Theorem an32 799
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 647 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 798 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 448 . 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 367
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 369
This theorem is referenced by:  an32s  805  3anan32  986  indifdir  3706  inrab2  3723  reupick  3734  difxp  5249  resco  5327  imadif  5644  respreima  5994  dff1o6  6162  dfoprab2  6324  f11o  6746  mpt2curryd  7001  xpassen  7649  dfac5lem1  8536  kmlem3  8564  qbtwnre  11451  elioomnf  11673  modfsummod  13759  pcqcl  14589  tosso  15990  subgdmdprd  17401  opsrtoslem1  18468  pjfval2  19038  fvmptnn04if  19642  cmpcov2  20183  tx1cn  20402  tgphaus  20907  isms2  21245  elcncf1di  21691  elii1  21727  dvreslem  22605  dvdsflsumcom  23845  is2wlk  24984  cvnbtwn3  27620  ordtconlem1  28359  1stmbfm  28708  eulerpartlemn  28826  ballotlem2  28933  dfon3  30230  brsuccf  30279  brsegle2  30447  bddiblnc  31458  ftc1anc  31471  prtlem17  31899  lcvnbtwn3  32046  cvrnbtwn3  32294  islpln5  32552  islvol5  32596  lhpexle3  33029  dibelval3  34167  dihglb2  34362  pm11.6  36146  stoweidlem17  37167
  Copyright terms: Public domain W3C validator