Theorem an32 568

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 405	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
2		an12 567	. 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  574  3anan32  1020  indifdir  3487  inrab2  3506  reupick  3517  unidif0  4299  resco  5287  f11o  5668  respreima  5827  dff1o6  5972  dfoprab2  6125  xpassen  7118  enq0enq  7788  elioomnf  10349  modfsummod  12203  pcqcl  13063  ballotfilem2  13206  tx1cn  15293  isms2  15478  elcncf1di  15603