Theorem an4 508

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 486	. . 3 |- ((ps /\ (ch /\ th)) <-> (ch /\ (ps /\ th)))
2	1	anbi2i 482	. 2 |- ((ph /\ (ps /\ (ch /\ th))) <-> (ph /\ (ch /\ (ps /\ th))))
3		anass 441	. 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> (ph /\ (ps /\ (ch /\ th))))
4		anass 441	. 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 509  an4s 510  anandi 512  anandir 513  rnlem 775  an6 904  euan 1430  2eu1 1452  2eu4 1455  reeanv 1781  reu2 1933  rmo4 1936  opelxp 3220  inxp 3275  xp11 3482  fununi 3569  2elresin 3604  fun 3647  fin 3657  tfrlem7 3923  th3qlem1 4320  xpmapenlem5 4506  aceq5lem1 4745  zorn2lem6 4803  genpass 5124  distrlem5pr 5143  mulgt0sr 5226  divmul24t 5785  iooint 6373  creur 6743  creui 6744  replimt 6762  xpcn 7973  ocsh 9151  5oalem6 9599  cvnbtwn4t 10211  superpos 10276  cdj3 10363  qusp 10541

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