Theorem an4 505

Description: Rearrangement of 4 conjuncts.

Assertion

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

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 483	. . 3 |- ((ps /\ (ch /\ th)) <-> (ch /\ (ps /\ th)))
2	1	anbi2i 479	. 2 |- ((ph /\ (ps /\ (ch /\ th))) <-> (ph /\ (ch /\ (ps /\ th))))
3		anass 439	. 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> (ph /\ (ps /\ (ch /\ th))))
4		anass 439	. 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> (ph /\ (ch /\ (ps /\ th))))
5	2, 3, 4	3bitr4 183	1 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))

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

This theorem is referenced by:  an42 506  an4s 507  anandi 509  anandir 510  rnlem 771  an6 899  euan 1421  2eu1 1442  2eu4 1445  reeanv 1770  reu2 1920  rmo4 1923  opelxp 3204  inxp 3259  xp11 3463  fununi 3549  2elresin 3584  fun 3626  fin 3636  tfrlem7 3902  th3qlem1 4298  xpmapenlem5 4480  abfii2 4536  aceq5lem1 4707  zorn2lem6 4765  genpass 5084  distrlem5pr 5103  mulgt0sr 5186  divmul24t 5739  iooint 6309  creur 6673  creui 6674  replimt 6692  xpcn 7910  circcltOLD 8656  ocsh 9072  5oalem6 9521  cvnbtwn4t 10126  superpos 10189  cdj3 10273  qusp 10430

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