Theorem bnj982

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj982.1	|- ( ph -> A. x ph )
	bnj982.2	|- ( ps -> A. x ps )
	bnj982.3	|- ( ch -> A. x ch )
	bnj982.4	|- ( th -> A. x th )
Assertion	bnj982	|- ( ( ph /\ ps /\ ch /\ th ) -> A. x ( ph /\ ps /\ ch /\ th ) )

Proof

Step	Hyp	Ref	Expression
1		bnj982.1	|- ( ph -> A. x ph )
2		bnj982.2	|- ( ps -> A. x ps )
3		bnj982.3	|- ( ch -> A. x ch )
4		bnj982.4	|- ( th -> A. x th )
5		df-bnj17	|- ( ( ph /\ ps /\ ch /\ th ) <-> ( ( ph /\ ps /\ ch ) /\ th ) )
6	1 2 3	hb3an	|- ( ( ph /\ ps /\ ch ) -> A. x ( ph /\ ps /\ ch ) )
7	6 4	hban	|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> A. x ( ( ph /\ ps /\ ch ) /\ th ) )
8	5 7	hbxfrbi	|- ( ( ph /\ ps /\ ch /\ th ) -> A. x ( ph /\ ps /\ ch /\ th ) )