Theorem an4 388

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

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

This theorem is referenced by:  an42 389  an4s 390  anandi 392  anandir 393  rnlem 579  an6 638  euanv 1053  2eu1 1067  2eu4 1070  reeanv 1316  reu2 1338  opelxp 2452  inxp 2496  fununi 2705  2elresin 2733  fun 2763  fin 2770  f1oco 2816  tfrlem7 2955  th3qlem1 3250  xpmapenlem5 3395  aceq5lem1 3558  zornlem6 3608  genpass 3906  distrlem5pr 3925  mulgt0sr 4008  axnegex 4078  creur 4532  creui 4533  replimt 4798  ocsh 5164  shscl 5282  5oalem6 5549  cvnbtwn4t 5721

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