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 ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an32s  574  3anan32  1020  indifdir  3487  inrab2  3506  reupick  3517  unidif0  4304  resco  5292  f11o  5673  respreima  5836  dff1o6  5982  dfoprab2  6135  xpassen  7128  enq0enq  7798  elioomnf  10370  modfsummod  12225  pcqcl  13085  ballotfilem2  13228  tx1cn  15370  isms2  15555  elcncf1di  15680