(𝐴⊐𝐵)⊐ ((𝐴⊐(𝐵⊐𝐶))⊐(𝐴⊐𝐶))
(A⊐B)⊐ ((A⊐(B⊐C))⊐(A⊐C))
(A→B)→ ((A→(B→C))→(A→C))
𝐴⊐(𝐵⊐𝐴∧𝐵)
A⊐(B⊐A∧B)
A→(B→A∧B)
(𝐴⊐𝐶)⊐((𝐵⊐𝐶)⊐(𝐴∨𝐵⊐𝐶))
(A⊐C)⊐((B⊐C)⊐(A∨B⊐C))
(A→C)→((B→C)→(A∨B→C))
(𝐴⊐𝐵)⊐ ((𝐴⊐ ⇁𝐵)⊐⇁𝐴)
(A⊐B)⊐ ((A⊐ ⇁B)⊐⇁A)
(A→B)→ ((A→ ⇁B)→⇁A)
⇁𝐴⊐(𝐴⊐𝐵)
⇁A⊐(A⊐B)
⇁A→(A→B)
∀𝑥𝑃𝑥⊐𝑃𝑡
∀xPx⊐Pt
forall xPx→Pt
𝑃𝑡⊐∃𝑥𝑃𝑥
Pt⊐∃xPx
Pt→existsxPx