Editing Hypothetical syllogism (section)

===Proof===
An example of the proofs of these theorems in such systems is given below.  We use two of the three axioms used in [[Propositional_calculus#Łukasiewicz's P2|one of the popular systems]] described by [[Jan Łukasiewicz]].
The proofs relies on two out of the three axioms of this system:
:(A1) <math>\phi \to \left( \psi \to \phi \right) </math>
:(A2) <math>\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to  \left( \phi \to \xi \right) \right)</math>

The proof of the (HS1) is as follows:
:(1) <math>((p\to(q \to r)) \to ((p \to q) \to (p \to r))) \to ((q \to r) \to ((p\to(q \to r)) \to ((p \to q) \to (p \to r))))</math> &nbsp; &nbsp; &nbsp; (instance of (A1))
:(2) <math>(p\to(q \to r)) \to ((p \to q) \to (p \to r))</math> &nbsp; &nbsp; &nbsp; (instance of (A2))
:(3) <math>(q \to r) \to ((p\to(q \to r)) \to ((p \to q) \to (p \to r)))</math> &nbsp; &nbsp; &nbsp; (from (1) and (2) by [[modus ponens]])
:(4) <math>((q \to r) \to ((p\to(q \to r)) \to ((p \to q) \to (p \to r))))\to (((q \to r) \to (p\to(q \to r))) \to ((q \to r)\to((p \to q) \to(p \to r))))</math> &nbsp; &nbsp; &nbsp; (instance of (A2))
:(5) <math>((q \to r) \to (p\to(q \to r))) \to ((q \to r)\to((p \to q) \to(p \to r)))</math> &nbsp; &nbsp; &nbsp; (from (3) and (4) by [[modus ponens]])
:(6) <math>(q \to r) \to (p\to(q \to r))</math> &nbsp; &nbsp; &nbsp; (instance of (A1))
:(7) <math>(q \to r)\to((p \to q) \to(p \to r))</math> (from (5) and (6) by [[modus ponens]])

The proof of the (HS2) is given [[Hilbert_system#Some_useful_theorems_and_their_proofs|here]].