Definition df-bnj17 30753

Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

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	w-bnj17 30752	. 2 wff ( ph /\ ps /\ ch /\ th )
6	1, 2, 3	w3a 1037	. . 3 wff ( ph /\ ps /\ ch )
7	6, 4	wa 384	. 2 wff ( ( ph /\ ps /\ ch ) /\ th )
8	5, 7	wb 196	1 wff ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )

This definition is referenced by:  bnj248  30766  bnj250  30767  bnj258  30774  bnj268  30775  bnj291  30777  bnj312  30778  bnj446  30783  bnj645  30820  bnj658  30821  bnj887  30835  bnj919  30837  bnj945  30844  bnj951  30846  bnj982  30849  bnj1019  30850  bnj518  30956  bnj571  30976  bnj594  30982  bnj916  31003  bnj966  31014  bnj967  31015  bnj1006  31029  bnj1018  31032  bnj1040  31040  bnj1174  31071  bnj1175  31072  bnj1311  31092