Theorem an4 588

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 563	. . 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  589  an4s  592  anandi  594  anandir  595  rnlem  984  an6  1357  2eu4  2173  reean  2702  reu2  2994  rmo4  2999  rmo3f  3003  rmo3  3124  inxp  4864  xp11m  5175  fununi  5398  fun  5508  resoprab2  6118  xporderlem  6396  poxp  6397  th3qlem1  6806  enq0enq  7651  enq0tr  7654  genpdisj  7743  cju  9141  elfzo2  10385  iooinsup  11839  summodc  11946  prodmodc  12141  issubmd  13559  dvdsrtr  14118  domnmuln0  14290  txbasval  14994  txcnp  14998  txlm  15006