Theorem bnj1096

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

	Ref	Expression
Hypotheses	bnj1096.1	|- ( ph -> A. x ph )
	bnj1096.2	|- ( ps <-> ( ch /\ th /\ ta /\ ph ) )
Assertion	bnj1096	|- ( ps -> A. x ps )

Proof

Step	Hyp	Ref	Expression
1		bnj1096.1	|- ( ph -> A. x ph )
2		bnj1096.2	|- ( ps <-> ( ch /\ th /\ ta /\ ph ) )
3		ax-5	|- ( ch -> A. x ch )
4		ax-5	|- ( th -> A. x th )
5		ax-5	|- ( ta -> A. x ta )
6	3 4 5 1	bnj982	|- ( ( ch /\ th /\ ta /\ ph ) -> A. x ( ch /\ th /\ ta /\ ph ) )
7	2 6	hbxfrbi	|- ( ps -> A. x ps )