Definition df-bnj17 12851

Description: Define the 4-way conjunction.

Assertion

Ref	Expression
df-bnj17	|- ((ph /\ ps /\ ch /\ th) <-> ((ph /\ ps /\ ch) /\ th))

Detailed syntax breakdown of Definition df-bnj17

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4		wth	. . 3 wff th
5	1, 2, 3, 4	syn-bnj17 12850	. 2 wff (ph /\ ps /\ ch /\ th)
6	1, 2, 3	w3a 1102	. . 3 wff (ph /\ ps /\ ch)
7	6, 4	wa 337	. 2 wff ((ph /\ ps /\ ch) /\ th)
8	5, 7	wb 219	1 wff ((ph /\ ps /\ ch /\ th) <-> ((ph /\ ps /\ ch) /\ th))

This definition is referenced by:  bnj248 12907  bnj249 12908  bnj258 12917  bnj268 12927  bnj269 12928  bnj280 12939  bnj291 12950  bnj302 12961  bnj312 12971  bnj313 12972  bnj324 12983  bnj335 12994  bnj346 13005  bnj357 13016  bnj368 13027  bnj379 13038  bnj390 13049  bnj401 13060  bnj412 13071  bnj423 13082  bnj435 13093  bnj446 13104  bnj457 13115  bnj468 13126  bnj480 13137  bnj491 13148  bnj501 13159  bnj645 13351  bnj658 13364  bnj887 13581  bnj913 13594  bnj951 13619  bnj982 13635  bnj1019 13649  bnj1046 13658  bnj1163 13726  bnj1305 13819  bnj518 14031  bnj557 14052  bnj571 14060  bnj594 14071  bnj966 14119  bnj967 14120  bnj1002 14138  bnj1017 14148  bnj1067 14170  bnj1174 14213

Copyright terms: Public domain