雑感・音楽等

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

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

com12 - Metamath Proof Explorer
com12 - Intuitionistic Logic Explorer

Hypothesis

Ref Expression
com12.1 ⊢(𝜑→(𝜓→𝜒))

Assertion

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


Proof of Theorem com12

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