Theorem an6 1308

Description: Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)

Assertion

Ref	Expression
an6

Proof of Theorem an6

Step	Hyp	Ref	Expression
1		an4 824	. . 3
2		an4 824	. . . 4
3	2	anbi1i 695	. . 3
4	1, 3	bitri 249	. 2
5		df-3an 975	. . 3
6		df-3an 975	. . 3
7	5, 6	anbi12i 697	. 2
8		df-3an 975	. 2
9	4, 7, 8	3bitr4i 277	1

Syntax hints:  <->wb 184  /\wa 369  /\w3a 973

This theorem is referenced by:  3an6  1309  ltdiv2OLD  10456  elfzuzb  11711  ptbasin  20078  iimulcl  21437  nb3grapr  24453  nb3grapr2  24454  txpcon  28677  fzadd2  30234  paddasslem9  35552  paddasslem10  35553

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 185  df-an 371  df-3an 975