φ
QED
φ
(
quod erat demonstrandum
)
⊥
EFQ
φ
(
ex falso quodlibet
)
ENV
⊤
(
ex nihilo verum
)
φ ∧ ψ
Ext
φ
(
extraction
)
φ ∧ ψ
Ext
ψ
(
extraction
)
φ
ψ
Cnj
φ ∧ ψ
(
conjunction
)