Theorem an4 517

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 495	. . 3 |- ((ps /\ (ch /\ th)) <-> (ch /\ (ps /\ th)))
2	1	anbi2i 491	. 2 |- ((ph /\ (ps /\ (ch /\ th))) <-> (ph /\ (ch /\ (ps /\ th))))
3		anass 450	. 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> (ph /\ (ps /\ (ch /\ th))))
4		anass 450	. 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> (ph /\ (ch /\ (ps /\ th))))
5	2, 3, 4	3bitr4i 190	1 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))

Syntax hints:   <-> wb 153   /\ wa 230

This theorem is referenced by:  an42 518  an4s 519  anandi 521  anandir 522  rnlem 785  an6 914  euan 1470  2eu1 1492  2eu4 1495  reeanv 1825  reu2 1977  rmo4 1980  opelxp 3271  inxp 3326  xp11 3533  fununi 3620  2elresin 3655  fun 3698  fin 3708  tfrlem7 3975  th3qlem1 4375  xpmapenlem5 4565  abfii2 4622  aceq5lem1 4797  zorn2lem6 4855  genpass 5177  distrlem5pr 5196  mulgt0sr 5279  divmul24 5841  iooin 6397  creur 6832  creui 6833  replim 6851  xpcn 8061  ocsh 9239  5oalem6 9687  cvnbtwn4 10300  superpos 10365  cdj3i 10452  qusp 10649

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 154  df-an 232

Copyright terms: Public domain