Metamath Proof Explorer

Theorem lttr

Description: Alias for axlttrn , for naming consistency with lttri . New proofs should generally use this instead of ax-pre-lttrn . (Contributed by NM, 10-Mar-2008)

		Ref	Expression
	Assertion	lttr	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$

Proof

Step	Hyp	Ref	Expression
1		axlttrn	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < B \land B < C) \to A < C)$