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

Theorem an32 798
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 797 . 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  804  3anan32  986  indifdir  3739  inrab2  3756  reupick  3767  difxp  5421  resco  5501  imadif  5653  respreima  6001  dff1o6  6166  dfoprab2  6328  f11o  6747  mpt2curryd  7000  xpassen  7613  dfac5lem1  8507  kmlem3  8535  qbtwnre  11409  elioomnf  11630  modfsummod  13590  pcqcl  14362  tosso  15645  subgdmdprd  17060  opsrtoslem1  18127  pjfval2  18718  fvmptnn04if  19328  cmpcov2  19868  tx1cn  20088  tgphaus  20593  isms2  20931  elcncf1di  21377  elii1  21413  dvreslem  22291  dvdsflsumcom  23442  is2wlk  24545  cvnbtwn3  27185  ordtconlem1  27884  1stmbfm  28209  eulerpartlemn  28298  ballotlem2  28405  dfon3  29518  brsegle2  29735  bddiblnc  30061  ftc1anc  30074  prtlem17  30593  pm11.6  31252  stoweidlem17  31753  lcvnbtwn3  34628  cvrnbtwn3  34876  islpln5  35134  islvol5  35178  lhpexle3  35611  dibelval3  36749  dihglb2  36944
  Copyright terms: Public domain W3C validator