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  590  anandi  592  anandir  593  rnlem  982  an6  1355  2eu4  2171  reean  2700  reu2  2991  rmo4  2996  rmo3f  3000  rmo3  3121  inxp  4856  xp11m  5167  fununi  5389  fun  5497  resoprab2  6101  xporderlem  6377  poxp  6378  th3qlem1  6784  enq0enq  7618  enq0tr  7621  genpdisj  7710  cju  9108  elfzo2  10346  iooinsup  11788  summodc  11894  prodmodc  12089  issubmd  13507  dvdsrtr  14065  domnmuln0  14237  txbasval  14941  txcnp  14945  txlm  14953