雑感・音楽等

音楽・数学・プログラミングに関する,思い付き・雑感を記す.

命題論理のメモ "Theorem syl5"の証明

syl5 - Metamath Proof Explorer
syl5 - Intuitionistic Logic Explorer


Hypothesis

Ref Expression
syl5.1 ⊢(𝜑→𝜓)
syl5.2 ⊢(𝜒→(𝜓→𝜃))

Assertion

Ref Expression
syl5 ⊢(𝜒→(𝜑→𝜃))


Proof of Theorem com12

Step Hyp Ref Expression
1 syl5.1 ⊢(𝜑→𝜓)
2 1 a1i ⊢(𝜒→(𝜑→𝜓))
3 syl5.2 ⊢(𝜒→(𝜓→𝜃))
4 3 a1i ⊢(𝜒→(𝜑→(𝜓→𝜃)))
5 4 a2d ⊢(𝜒→((𝜑→𝜓)→(𝜑→𝜃)))
6 5 a2i ⊢( (𝜒→(𝜑→𝜓)) → (𝜒→(𝜑→𝜃)) )
7 2, 6 ax-mp ⊢(𝜒→(𝜑→𝜃))