Theorem cgrtr4d

Description: Deduction form of axcgrtr . (Contributed by Scott Fenton, 13-Oct-2013)

	Ref	Expression
Hypotheses	cgrtr4d.1	$$⊢\phi \to N\in \mathbb{N}$$
	cgrtr4d.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
	cgrtr4d.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
	cgrtr4d.4	$$⊢\phi \to C\in 𝔼\left(N\right)$$
	cgrtr4d.5	$$⊢\phi \to D\in 𝔼\left(N\right)$$
	cgrtr4d.6	$$⊢\phi \to E\in 𝔼\left(N\right)$$
	cgrtr4d.7	$$⊢\phi \to F\in 𝔼\left(N\right)$$
	cgrtr4d.8	$$⊢\phi \to ⟨A,B⟩\mathrm{Cgr}⟨C,D⟩$$
	cgrtr4d.9	$$⊢\phi \to ⟨A,B⟩\mathrm{Cgr}⟨E,F⟩$$
Assertion	cgrtr4d	$$⊢\phi \to ⟨C,D⟩\mathrm{Cgr}⟨E,F⟩$$

Proof

Step	Hyp	Ref	Expression
1		cgrtr4d.1	$$⊢\phi \to N\in \mathbb{N}$$
2		cgrtr4d.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
3		cgrtr4d.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
4		cgrtr4d.4	$$⊢\phi \to C\in 𝔼\left(N\right)$$
5		cgrtr4d.5	$$⊢\phi \to D\in 𝔼\left(N\right)$$
6		cgrtr4d.6	$$⊢\phi \to E\in 𝔼\left(N\right)$$
7		cgrtr4d.7	$$⊢\phi \to F\in 𝔼\left(N\right)$$
8		cgrtr4d.8	$$⊢\phi \to ⟨A,B⟩\mathrm{Cgr}⟨C,D⟩$$
9		cgrtr4d.9	$$⊢\phi \to ⟨A,B⟩\mathrm{Cgr}⟨E,F⟩$$
10		axcgrtr	$$⊢\left(N\in \mathbb{N}\wedge \left(A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\wedge C\in 𝔼\left(N\right)\right)\wedge \left(D\in 𝔼\left(N\right)\wedge E\in 𝔼\left(N\right)\wedge F\in 𝔼\left(N\right)\right)\right)\to \left(\left(⟨A,B⟩\mathrm{Cgr}⟨C,D⟩\wedge ⟨A,B⟩\mathrm{Cgr}⟨E,F⟩\right)\to ⟨C,D⟩\mathrm{Cgr}⟨E,F⟩\right)$$
11	1 2 3 4 5 6 7 10	syl133anc	$$⊢\phi \to \left(\left(⟨A,B⟩\mathrm{Cgr}⟨C,D⟩\wedge ⟨A,B⟩\mathrm{Cgr}⟨E,F⟩\right)\to ⟨C,D⟩\mathrm{Cgr}⟨E,F⟩\right)$$
12	8 9 11	mp2and	$$⊢\phi \to ⟨C,D⟩\mathrm{Cgr}⟨E,F⟩$$