Theorem an23 485

Description: A rearrangement of conjuncts.

Assertion

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

Proof of Theorem an23

Step	Hyp	Ref	Expression
1		ancom 435	. . 3 |- ((ps /\ ch) <-> (ch /\ ps))
2	1	anbi2i 480	. 2 |- ((ph /\ (ps /\ ch)) <-> (ph /\ (ch /\ ps)))
3		anass 439	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
4		anass 439	. 2 |- (((ph /\ ch) /\ ps) <-> (ph /\ (ch /\ ps)))
5	2, 3, 4	3bitr4 183	1 |- (((ph /\ ps) /\ ch) <-> ((ph /\ ch) /\ ps))

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  an1rs 489  inrab2 2268  reupick 2275  resco 3492  imadif 3566  f1o3 3685  f11o 3703  f1ofv 3868  tz7.49c 3951  dfoprab2 3982  xpcomen 4425  xpassen 4427  aceq5lem1 4715  kmlem3 4747  1idpr 5113  elcncf1d 7213  infxpidmlem7 7509  infxpidmlem9 7511  cvnbtwn3t 10153

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain