Theorem issubgoilem

Description: Lemma for hhssabloilem . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	issubgoilem.1	$$⊢\left(x\in Y\wedge y\in Y\right)\to xHy=xGy$$
Assertion	issubgoilem	$$⊢\left(A\in Y\wedge B\in Y\right)\to AHB=AGB$$

Proof

Step	Hyp	Ref	Expression
1		issubgoilem.1	$$⊢\left(x\in Y\wedge y\in Y\right)\to xHy=xGy$$
2		oveq1	$$⊢x=A\to xHy=AHy$$
3		oveq1	$$⊢x=A\to xGy=AGy$$
4	2 3	eqeq12d	$$⊢x=A\to \left(xHy=xGy\leftrightarrow AHy=AGy\right)$$
5		oveq2	$$⊢y=B\to AHy=AHB$$
6		oveq2	$$⊢y=B\to AGy=AGB$$
7	5 6	eqeq12d	$$⊢y=B\to \left(AHy=AGy\leftrightarrow AHB=AGB\right)$$
8	4 7 1	vtocl2ga	$$⊢\left(A\in Y\wedge B\in Y\right)\to AHB=AGB$$