Theorem an23 487

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 437	. . 3 |- ((ps /\ ch) <-> (ch /\ ps))
2	1	anbi2i 482	. 2 |- ((ph /\ (ps /\ ch)) <-> (ph /\ (ch /\ ps)))
3		anass 441	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
4		anass 441	. 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 491  inrab2 2275  reupick 2282  resco 3506  imadif 3580  f1o3 3700  f11o 3718  f1ofv 3883  tz7.49c 3966  dfoprab2 3997  xpcomen 4445  xpassen 4447  aceq5lem1 4745  kmlem3 4777  1idpr 5145  elcncf1d 7270  infxpidmlem7 7559  infxpidmlem9 7561  cvnbtwn3t 10210

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