Can I imply something by omitting two operands of an 'or-operation'?

Question

I've got a question about the use of implications during the process of proving something. I will get more specific. I tried to solve the following problem:

The solution is straight forward. Show that L satisfies all axioms of a poset under the given conditions. I've got stuck proving that $a \le b \wedge b\le c \implies a \le c$.

Here's my attempt to present a solution.

$a \le b \wedge b\le c$

$\iff (\ a = b \vee a < b)\ \wedge (\ b = c \vee b < c)\ $

$\iff [\ (\ a = b \vee a < b)\ \wedge (\ b = c )\ ]\ \vee [\ (\ a = b \vee a < b)\ \wedge (\ b < c )\ ]\ $

$\iff \langle [\ (\ a = b )\ \wedge (\ b=c)\ ]\ \vee [\ (\ a < b )\ \wedge (\ b = c )\ ]\ \rangle \vee \langle [\ (\ a = b)\ \wedge (\ b < c )\ ]\ \vee [\ (\ a < c)\ \wedge (b < c) ]\ \rangle $

$\iff [\ (\ a = b )\ \wedge (\ b=c)\ ]\ \vee [\ (\ a < c)\ \wedge (b < c) ] \vee [\ (\ a < b )\ \wedge (\ b = c )\ ]\ \vee [\ (\ a = b)\ \wedge (\ b < c )\ ]\ \ $

$\implies [\ (\ a = b )\ \wedge (\ b=c)\ ]\ \vee [\ (\ a < c)\ \wedge (b < c) ] \implies (a = c) \wedge (a<c) \implies a \le c$

Now, while this seems to lead to a correct solution, I am very unsure about the first implication I've made by omitting two of the []'s. Can somebody tell meif this is correct? And if not, what would be the correct formal proof?

Answer 1

Your next-to-last line reads: $$[(a=b) \wedge (b=c) ] \vee [(a<c) \wedge (b<c)] \vee [(a<b) \wedge (b=c)] \vee [(a=b) \wedge (b<c)] \enspace.$$

What is left is to show that all four disjuncts imply $a \leq c$.

• $[(a=b) \wedge (b=c)]$ implies $a=c$ by transitivity of equality; $a=c$, in turn, implies $a \leq c$.
• $[(a<c) \wedge (b<c)]$ implies $a<c$ by transitivity of $<$; $a<c$, in turn, implies $a \leq c$.
• $[(a<b) \wedge (b=c)]$ also implies $a<c$, hence $a \leq c$.
• $[(a=b) \wedge (b<c)]$ also implies $a<c$, hence $a \leq c$.

As to the question whether you can omit two disjuncts, the answer, if I understand the question, is no. You cannot focus on the cases that support the conclusion you are trying to prove and ignore the others.