2.(𝐴⊐𝐵)⊐ ((𝐴⊐(𝐵⊐𝐶))⊐(𝐴⊐𝐶))
(A⊐B)⊐ ((A⊐(B⊐C))⊐(A⊐C))
(A→B)→ ((A→(B→C))→(A→C))PL.FL.02IL.K.02axiom✹
3.𝐴⊐(𝐵⊐𝐴∧𝐵)
A⊐(B⊐A∧B)
A→(B→A∧B)IL.K.03axiom✹
4.𝐴∧𝐵⊐𝐴
A∧B⊐A
A∧B→AIL.K.04axiom✹
5.𝐴∧𝐵⊐𝐵
A∧B⊐B
A∧B→BIL.K.05axiom✹
6.𝐴⊐𝐴∨𝐵
A⊐A∨B
A→A∨BIL.K.06axiom✹
7.𝐵⊐𝐴∨𝐵
B⊐A∨B
B→A∨BIL.K.07axiom✹
8.(𝐴⊐𝐶)⊐((𝐵⊐𝐶)⊐(𝐴∨𝐵⊐𝐶))
(A⊐C)⊐((B⊐C)⊐(A∨B⊐C))
(A→C)→((B→C)→(A∨B→C))IL.K.08axiom✹
9.(𝐴⊐𝐵)⊐ ((𝐴⊐ ⇁𝐵)⊐⇁𝐴)
(A⊐B)⊐ ((A⊐ ⇁B)⊐⇁A)
(A→B)→ ((A→ ⇁B)→⇁A)IL.K.09axiom✹
10.⇁𝐴⊐(𝐴⊐𝐵)
⇁A⊐(A⊐B)
⇁A→(A→B)IL.K.10axiom✹
11.∀𝑥𝑃𝑥⊐𝑃𝑡
∀xPx⊐Pt
forall xPx→PtIL.K.11axiom✹
12.𝑃𝑡⊐∃𝑥𝑃𝑥
Pt⊐∃xPx
Pt→forsome existsxPxIL.K.12axiom✹