Theorem an23 371

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 333	. . 3 |- ((ps /\ ch) <-> (ch /\ ps))
2	1	anbi2i 367	. 2 |- ((ph /\ (ps /\ ch)) <-> (ph /\ (ch /\ ps)))
3		anass 336	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
4		anass 336	. 2 |- (((ph /\ ch) /\ ps) <-> (ph /\ (ch /\ ps)))
5	2, 3, 4	3bitr4 158	1 |- (((ph /\ ps) /\ ch) <-> ((ph /\ ch) /\ ps))

Syntax hints:   <-> wb 127   /\ wa 196

This theorem is referenced by:  an1rs 373  reupick 1578  imadif 2714  f1o3 2805  f11o 2821  tz7.49c 2998  dfoprab2 3021  xpcomen 3343  xpassen 3344  aceq5lem1 3558  kmlem3 3582  1idpr 3927  infxpidmlem7 4939  infxpidmlem9 4941  cvnbtwn3t 5720

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org