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

Theorem an32 774
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 631 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
2 an12 773 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ps  /\  ( ph  /\  ch ) ) )
3 ancom 438 . 2  |-  ( ( ps  /\  ( ph  /\ 
ch ) )  <->  ( ( ph  /\  ch )  /\  ps ) )
41, 2, 33bitri 263 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ph  /\  ch )  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an32s  780  3anan32  948  indifdir  3589  inrab2  3606  reupick  3617  resco  5366  imadif  5520  f11o  5700  respreima  5851  dff1o6  6005  dfoprab2  6113  difxp  6372  xpassen  7194  dfac5lem1  7996  kmlem3  8024  qbtwnre  10777  elioomnf  10991  pcqcl  13222  tosso  14457  subgdmdprd  15584  opsrtoslem1  16536  pjfval2  16928  cmpcov2  17445  tx1cn  17633  tgphaus  18138  isms2  18472  elcncf1di  18917  elii1  18952  dvreslem  19788  dvdsflsumcom  20965  is2wlk  21557  cvnbtwn3  23783  1stmbfm  24602  ballotlem2  24738  dfon3  25729  brsegle2  26035  bddiblnc  26265  ftc1anc  26278  prtlem17  26716  pm11.6  27559  stoweidlem17  27733  lcvnbtwn3  29763  cvrnbtwn3  30011  islpln5  30269  islvol5  30313  lhpexle3  30746  dibelval3  31882  dihglb2  32077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator