Theorem 3anan32 1050

Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Assertion

Ref	Expression
3anan32	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )

Proof of Theorem 3anan32

Step	Hyp	Ref	Expression
1		df-3an 1039	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		an32 839	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )
3	1, 2	bitri 264	1 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  anandi3r  1053  dff1o3  6143  bropfvvvvlem  7256  tz7.49c  7541  ispos2  16948  lbsacsbs  19156  obslbs  20074  islbs4  20171  leordtvallem1  21014  trfbas2  21647  isclmp  22897  lssbn  23148  sineq0  24273  dchrelbas3  24963  nb3grpr2  26285  uspgr2wlkeq  26542  2spthd  26837  frgr2wwlkeu  27191  elicoelioo  29540  cndprobprob  30500  bnj543  30963  elno3  31808  ellimits  32017