命題論理のメモ "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	⊢(𝜓→(𝜑→𝜒))