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

Theorem an32 806
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 654 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 805 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 452 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 275 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  an32s  812  3anan32  996  indifdir  3698  inrab2  3715  reupick  3726  difxp  5260  resco  5338  imadif  5656  respreima  6007  dff1o6  6172  dfoprab2  6334  f11o  6752  mpt2curryd  7013  xpassen  7663  dfac5lem1  8551  kmlem3  8579  qbtwnre  11489  elioomnf  11726  modfsummod  13847  pcqcl  14799  tosso  16275  subgdmdprd  17660  opsrtoslem1  18700  pjfval2  19265  fvmptnn04if  19866  cmpcov2  20398  tx1cn  20617  tgphaus  21124  isms2  21458  elcncf1di  21920  elii1  21956  dvreslem  22857  dvdsflsumcom  24110  is2wlk  25288  cvnbtwn3  27934  ordtconlem1  28723  1stmbfm  29075  eulerpartlemn  29207  ballotlem2  29314  dfon3  30652  brsuccf  30701  brsegle2  30869  poimirlem25  31958  bddiblnc  32005  ftc1anc  32018  prtlem17  32442  lcvnbtwn3  32588  cvrnbtwn3  32836  islpln5  33094  islvol5  33138  lhpexle3  33571  dibelval3  34709  dihglb2  34904  pm11.6  36736  stoweidlem17  37871  upgr2wlk  39646
  Copyright terms: Public domain W3C validator