Theorem aevdemo

Description: Proof illustrating the comment of aev2 . (Contributed by BJ, 30-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	aevdemo	$$⊢\forall xx=y\to \left(\left(\exists a\forall bc=d\vee \exists ef=g\right)\wedge \forall h\left(i=j\to k=l\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		aev	$$⊢\forall xx=y\to \forall ef=g$$
2	1	19.2d	$$⊢\forall xx=y\to \exists ef=g$$
3	2	olcd	$$⊢\forall xx=y\to \left(\exists a\forall bc=d\vee \exists ef=g\right)$$
4		aev	$$⊢\forall xx=y\to \forall mm=n$$
5		aeveq	$$⊢\forall mm=n\to k=l$$
6	5	a1d	$$⊢\forall mm=n\to \left(i=j\to k=l\right)$$
7	6	alrimiv	$$⊢\forall mm=n\to \forall h\left(i=j\to k=l\right)$$
8	4 7	syl	$$⊢\forall xx=y\to \forall h\left(i=j\to k=l\right)$$
9	3 8	jca	$$⊢\forall xx=y\to \left(\left(\exists a\forall bc=d\vee \exists ef=g\right)\wedge \forall h\left(i=j\to k=l\right)\right)$$