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

Theorem an32 815
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 661 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 814 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 457 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 279 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  an32s  821  3anan32  1019  indifdir  3690  inrab2  3707  reupick  3718  difxp  5267  resco  5346  imadif  5668  respreima  6024  dff1o6  6192  dfoprab2  6356  f11o  6774  mpt2curryd  7034  xpassen  7684  dfac5lem1  8572  kmlem3  8600  qbtwnre  11515  elioomnf  11754  modfsummod  13931  pcqcl  14885  tosso  16360  subgdmdprd  17745  opsrtoslem1  18784  pjfval2  19349  fvmptnn04if  19950  cmpcov2  20482  tx1cn  20701  tgphaus  21209  isms2  21543  elcncf1di  22005  elii1  22041  dvreslem  22943  dvdsflsumcom  24196  is2wlk  25374  cvnbtwn3  28022  ordtconlem1  28804  1stmbfm  29155  eulerpartlemn  29287  ballotlem2  29394  dfon3  30730  brsuccf  30779  brsegle2  30947  poimirlem25  32029  bddiblnc  32076  ftc1anc  32089  prtlem17  32512  lcvnbtwn3  32665  cvrnbtwn3  32913  islpln5  33171  islvol5  33215  lhpexle3  33648  dibelval3  34786  dihglb2  34981  pm11.6  36812  stoweidlem17  37989  upgr2wlk  39863  upgrtrls  39897  upgristrl  39898
  Copyright terms: Public domain W3C validator