Theorem cgrrflxd

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

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

Proof

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