雑感等

音楽,数学,語学,その他に関するメモを記す.

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

a1d - Metamath Proof Explorer

a1d - Intuitionistic Logic Explorer

Hypothesis

Ref Expression
a1d.1 ⊢(𝜑→𝜓)

Assertion

Ref Expression
a1d ⊢(𝜑→(𝜒→𝜓))

Proof of Theorem a1d

Step Hyp Ref Expression
1 ax-1 ⊢(𝜓→(𝜒→𝜓))
2 ax-1 ⊢( (𝜓→(𝜒→𝜓)) → (𝜑→(𝜓→(𝜒→𝜓))) )
3 1, 2 ax-mp ⊢(𝜑→(𝜓→(𝜒→𝜓)))
4 ax-2 ⊢( (𝜑→(𝜓→(𝜒→𝜓))) → ((𝜑→𝜓)→(𝜑→(𝜒→𝜓))) )
5 3, 4 ax-mp ⊢( (𝜑→𝜓) → (𝜑→(𝜒→𝜓)) )
6 a1d.1 ⊢(𝜑→𝜓)
7 5, 6 ax-mp ⊢(𝜑→(𝜒→𝜓))