Theorem an4 592

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 567	. . 3 |- ( ( ps /\ ( ch /\ th ) ) <-> ( ch /\ ( ps /\ th ) ) )
2	1	anbi2i 461	. 2 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) <-> ( ph /\ ( ch /\ ( ps /\ th ) ) ) )
3		anass 405	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ph /\ ( ps /\ ( ch /\ th ) ) ) )
4		anass 405	. 2 |- ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) <-> ( ph /\ ( ch /\ ( ps /\ th ) ) ) )
5	2, 3, 4	3bitr4i 212	1 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch ) /\ ( ps /\ th ) ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an42  593  an4s  596  anandi  598  anandir  599  rnlem  989  an6  1362  2eu4  2180  reean  2720  reu2  3014  rmo4  3019  rmo3f  3023  rmo3  3144  inxp  4914  xp11m  5226  fununi  5449  fun  5561  resoprab2  6185  xporderlem  6467  poxp  6468  th3qlem1  6911  enq0enq  7798  enq0tr  7801  genpdisj  7890  cju  9291  elfzo2  10557  iooinsup  12043  summodc  12150  prodmodc  12345  issubmd  13781  dvdsrtr  14408  domnmuln0  14582  txbasval  15368  txcnp  15372  txlm  15380