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  985  indifdir  3754  inrab2  3771  reupick  3782  difxp  5431  resco  5511  imadif  5663  respreima  6010  dff1o6  6169  dfoprab2  6327  f11o  6746  mpt2curryd  6998  xpassen  7611  dfac5lem1  8504  kmlem3  8532  qbtwnre  11398  elioomnf  11619  modfsummod  13571  pcqcl  14239  tosso  15523  subgdmdprd  16883  opsrtoslem1  17947  pjfval2  18535  cmpcov2  19684  tx1cn  19873  tgphaus  20378  isms2  20716  elcncf1di  21162  elii1  21198  dvreslem  22076  dvdsflsumcom  23220  is2wlk  24271  cvnbtwn3  26911  ordtconlem1  27570  1stmbfm  27899  eulerpartlemn  27988  ballotlem2  28095  dfon3  29147  brsegle2  29364  bddiblnc  29690  ftc1anc  29703  prtlem17  30249  pm11.6  30904  stoweidlem17  31345  lcvnbtwn3  33843  cvrnbtwn3  34091  islpln5  34349  islvol5  34393  lhpexle3  34826  dibelval3  35962  dihglb2  36157
  Copyright terms: Public domain W3C validator