Theorem cgrrflx2d

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

	Ref	Expression
Hypotheses	cgrrflx2d.1	$$⊢\phi \to N\in \mathbb{N}$$
	cgrrflx2d.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
	cgrrflx2d.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
Assertion	cgrrflx2d	$$⊢\phi \to ⟨A,B⟩\mathrm{Cgr}⟨B,A⟩$$

Proof

Step	Hyp	Ref	Expression
1		cgrrflx2d.1	$$⊢\phi \to N\in \mathbb{N}$$
2		cgrrflx2d.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
3		cgrrflx2d.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
4		axcgrrflx	$$⊢\left(N\in \mathbb{N}\wedge A\in 𝔼\left(N\right)\wedge B\in 𝔼\left(N\right)\right)\to ⟨A,B⟩\mathrm{Cgr}⟨B,A⟩$$
5	1 2 3 4	syl3anc	$$⊢\phi \to ⟨A,B⟩\mathrm{Cgr}⟨B,A⟩$$