Theorem btwncomand

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

	Ref	Expression
Hypotheses	btwncomand.1	$$⊢\phi \to N\in \mathbb{N}$$
	btwncomand.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
	btwncomand.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
	btwncomand.4	$$⊢\phi \to C\in 𝔼\left(N\right)$$
	btwncomand.5	$$⊢\left(\phi \wedge \psi \right)\to A\mathrm{Btwn}⟨B,C⟩$$
Assertion	btwncomand	$$⊢\left(\phi \wedge \psi \right)\to A\mathrm{Btwn}⟨C,B⟩$$

Proof

Step	Hyp	Ref	Expression
1		btwncomand.1	$$⊢\phi \to N\in \mathbb{N}$$
2		btwncomand.2	$$⊢\phi \to A\in 𝔼\left(N\right)$$
3		btwncomand.3	$$⊢\phi \to B\in 𝔼\left(N\right)$$
4		btwncomand.4	$$⊢\phi \to C\in 𝔼\left(N\right)$$
5		btwncomand.5	$$⊢\left(\phi \wedge \psi \right)\to A\mathrm{Btwn}⟨B,C⟩$$
6		btwncom	$$⊢\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)\right)\to \left(A\mathrm{Btwn}⟨B,C⟩\leftrightarrow A\mathrm{Btwn}⟨C,B⟩\right)$$
7	1 2 3 4 6	syl13anc	$$⊢\phi \to \left(A\mathrm{Btwn}⟨B,C⟩\leftrightarrow A\mathrm{Btwn}⟨C,B⟩\right)$$
8	7	adantr	$$⊢\left(\phi \wedge \psi \right)\to \left(A\mathrm{Btwn}⟨B,C⟩\leftrightarrow A\mathrm{Btwn}⟨C,B⟩\right)$$
9	5 8	mpbid	$$⊢\left(\phi \wedge \psi \right)\to A\mathrm{Btwn}⟨C,B⟩$$