Theorem an32 552

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 399	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
2		an12 551	. 2 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ps /\ ( ph /\ ch ) ) )
3		ancom 264	. 2 |- ( ( ps /\ ( ph /\ ch ) ) <-> ( ( ph /\ ch ) /\ ps ) )
4	1, 2, 3	3bitri 205	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an32s  558  3anan32  979  indifdir  3377  inrab2  3394  reupick  3405  unidif0  4145  resco  5107  f11o  5464  respreima  5612  dff1o6  5743  dfoprab2  5885  xpassen  6792  enq0enq  7368  elioomnf  9900  modfsummod  11395  pcqcl  12234  tx1cn  12869  isms2  13054  elcncf1di  13166