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 | ⊢(𝜓→(𝜑→𝜒)) |