# How to prove statements of the form $(A \implies B) \implies C$

This question grew out of this question, but my question is on the logic structure to a possible answer to that question.

In that question, the OP was trying to prove a statement of the form

$$(A \implies B) \implies C$$

The way I've learnt this, is that you assume the antedecent $(A \implies B)$ and prove the consequent $C$. My problem with this is that from the given antecedent, we cannot assume $A$, nor $B$, but only that $A$ implies $B$. Yet in the hint to the OP in that question, the answerer seems to reason like this:

"Assume $A$, and that $B$ follows from $A$, now prove C"

I can't justify to myself why I would be allowed to assume $A$. More broadly, what exactly can I use when proving these statements? Can I assume $A$ is true and that $B$ follows?

If I may ask for an example of a proof of some trivial statement in the style of everyday language ("All men are mortal" or the like), I'm sure this will clear up.

• You're right. The strategy you described can prove $A\to(A\to B)\to C$ or $(A\to B) \to (A\to C)$ not $(A\to B)\to C$.
– MJD
Oct 22, 2017 at 12:18
• The "trick" is that the theorem of the related question: "if (if ..., then ___), then $f$ is continuous" is not proved by logic alone. It is proved using the mathematical definition of continuity (and maybe also some additonal properties). This is shown by the fact that $(A \to B) \to C$ is not a "law of logic" i.e. a tautology. Oct 22, 2017 at 12:24
• The logic in the answer you link to is backwards in several ways -- do not take it as a model of valid proof structure! Oct 22, 2017 at 12:26
• @HenningMakholm This is exactly why I'm asking! What would be a model of a valid proof structure? Oct 22, 2017 at 12:33
• @Mauro: I'm not sure that plan of attack actually works here. I can't get the details to work out that way, and I suspect "sequential continuity implies continuity" is not constructively valid -- so one has to use something like contraposition in order to get there. Oct 22, 2017 at 13:18

To prove something in a logical theory $\mathfrak{T}$ such as $A\implies B$, one adjoins $A$ to the explicit axioms of $\mathfrak{T}$ and proves $B$ within the newly gained theory. In short, what you stated was right. $A\implies B$ is to be assumed, but nothing about $A$ or $B$.