Theorem an32 562

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

Step	Hyp	Ref	Expression
1		anass 401	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
2		an12 561	. 2 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )
3		ancom 266	. 2 |- ( ( ps /\ ( ph /\ ch ) ) <-> ( ( ph /\ ch ) /\ ps ) )
4	1, 2, 3	3bitri 206	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an32s  568  3anan32  992  indifdir  3433  inrab2  3450  reupick  3461  unidif0  4218  resco  5195  f11o  5566  respreima  5720  dff1o6  5857  dfoprab2  6004  xpassen  6939  enq0enq  7559  elioomnf  10105  modfsummod  11839  pcqcl  12699  tx1cn  14811  isms2  14996  elcncf1di  15121