Theorem an4 558

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an42  559  an4s  560  anandi  562  anandir  563  rnlem  943  an6  1282  2eu4  2068  reean  2573  reu2  2841  rmo4  2846  rmo3f  2850  rmo3  2968  inxp  4633  xp11m  4935  fununi  5149  fun  5253  resoprab2  5822  xporderlem  6082  poxp  6083  th3qlem1  6485  enq0enq  7187  enq0tr  7190  genpdisj  7279  cju  8629  elfzo2  9820  iooinsup  10938  summodc  11044  txbasval  12278  txcnp  12282  txlm  12290