Theorem an4 575

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 550	. . 3 |- ( ( ps /\ ( ch /\ th ) ) <-> ( ch /\ ( ps /\ th ) ) )
2	1	anbi2i 452	. 2 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) <-> ( ph /\ ( ch /\ ( ps /\ th ) ) ) )
3		anass 398	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ph /\ ( ps /\ ( ch /\ th ) ) ) )
4		anass 398	. 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an42  576  an4s  577  anandi  579  anandir  580  rnlem  960  an6  1299  2eu4  2092  reean  2599  reu2  2872  rmo4  2877  rmo3f  2881  rmo3  3000  inxp  4673  xp11m  4977  fununi  5191  fun  5295  resoprab2  5868  xporderlem  6128  poxp  6129  th3qlem1  6531  enq0enq  7239  enq0tr  7242  genpdisj  7331  cju  8719  elfzo2  9927  iooinsup  11046  summodc  11152  prodmodc  11347  txbasval  12436  txcnp  12440  txlm  12448