Theorem an4 797

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 772	. . 3 |- ((ps /\ (ch /\ th)) <-> (ch /\ (ps /\ th)))
2	1	anbi2i 675	. 2 |- ((ph /\ (ps /\ (ch /\ th))) <-> (ph /\ (ch /\ (ps /\ th))))
3		anass 630	. 2 |- (((ph /\ ps) /\ (ch /\ th)) <-> (ph /\ (ps /\ (ch /\ th))))
4		anass 630	. 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> (ph /\ (ch /\ (ps /\ th))))
5	2, 3, 4	3bitr4i 268	1 |- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))

Syntax hints:   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  an42  798  an4s  799  anandi  801  anandir  802  rnlem  931  an6  1261  2eu1  2284  2eu4  2287  reean  2778  reu2  3025  rmo4  3030  rmo3  3134  inxpk  4278  dfpw12  4302  ltfintr  4460  opelxp  4812  inxp  4864  xp11  5057  fununi  5161  2elresin  5195  fun  5237  resoprab2  5583  brtxp  5784  qrpprod  5837  fundmen  6044