Theorem an32 557

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 556	. 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  563  3anan32  984  indifdir  3383  inrab2  3400  reupick  3411  unidif0  4153  resco  5115  f11o  5475  respreima  5624  dff1o6  5755  dfoprab2  5900  xpassen  6808  enq0enq  7393  elioomnf  9925  modfsummod  11421  pcqcl  12260  tx1cn  13063  isms2  13248  elcncf1di  13360