Theorem an4 586

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)

Assertion

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

Proof of Theorem an4

Step	Hyp	Ref	Expression
1		an12 561	. . 3 |- ( ( ps /\ ( ch /\ th ) ) <-> ( ch /\ ( ps /\ th ) ) )
2	1	anbi2i 457	. 2 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) <-> ( ph /\ ( ch /\ ( ps /\ th ) ) ) )
3		anass 401	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ph /\ ( ps /\ ( ch /\ th ) ) ) )
4		anass 401	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) <-> ( ph /\ ( ch /\ ( ps /\ th ) ) ) )
5	2, 3, 4	3bitr4i 212	1 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an42  587  an4s  588  anandi  590  anandir  591  rnlem  978  an6  1332  2eu4  2138  reean  2666  reu2  2952  rmo4  2957  rmo3f  2961  rmo3  3081  inxp  4801  xp11m  5109  fununi  5327  fun  5433  resoprab2  6023  xporderlem  6298  poxp  6299  th3qlem1  6705  enq0enq  7515  enq0tr  7518  genpdisj  7607  cju  9005  elfzo2  10242  iooinsup  11459  summodc  11565  prodmodc  11760  issubmd  13176  dvdsrtr  13733  domnmuln0  13905  txbasval  14587  txcnp  14591  txlm  14599