Theorem bj-gabssd

Description: Inclusion of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-gabssd.nf	$$⊢\phi \to \forall x\phi$$
	bj-gabssd.c	$$⊢\phi \to A=B$$
	bj-gabssd.f	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	bj-gabssd	Could not format assertion : No typesetting found for |- ( ph -> {{ A | x | ps }} C_ {{ B | x | ch }} ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bj-gabssd.nf	$$⊢\phi \to \forall x\phi$$
2		bj-gabssd.c	$$⊢\phi \to A=B$$
3		bj-gabssd.f	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	2 3	jca	$$⊢\phi \to \left(A=B\wedge \left(\psi \to \chi \right)\right)$$
5	1 4	alrimih	$$⊢\phi \to \forall x\left(A=B\wedge \left(\psi \to \chi \right)\right)$$
6		bj-gabss	Could not format ( A. x ( A = B /\ ( ps -> ch ) ) -> {{ A | x | ps }} C_ {{ B | x | ch }} ) : No typesetting found for |- ( A. x ( A = B /\ ( ps -> ch ) ) -> {{ A | x | ps }} C_ {{ B | x | ch }} ) with typecode |-
7	5 6	syl	Could not format ( ph -> {{ A | x | ps }} C_ {{ B | x | ch }} ) : No typesetting found for |- ( ph -> {{ A | x | ps }} C_ {{ B | x | ch }} ) with typecode |-