Theorem inagne1

Description: Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021)

	Ref	Expression
Hypotheses	isinag.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	isinag.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	isinag.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	isinag.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	isinag.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	isinag.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	isinag.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	inagflat.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	inagswap.1	⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
Assertion	inagne1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		isinag.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		isinag.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		isinag.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		isinag.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5		isinag.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		isinag.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		isinag.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		inagflat.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
9		inagswap.1	⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
10	1 2 3 4 5 6 7 8	isinag	⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )
11	9 10	mpbid	⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
12	11	simpld	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) )
13	12	simp1d	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )