![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mt2 | Structured version Visualization version GIF version |
Description: A rule similar to modus tollens. Inference associated with con2i 139. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |
Ref | Expression |
---|---|
mt2.1 | ⊢ 𝜓 |
mt2.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
mt2 | ⊢ ¬ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mt2.1 | . . 3 ⊢ 𝜓 | |
2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → 𝜓) |
3 | mt2.2 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
4 | 2, 3 | pm2.65i 193 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: bijust0 203 ax6dgen 2117 nlim2 8511 infn0 9332 elirrv 9620 cardom 10010 0nnnALT 12280 nthruz 16230 hauspwdom 23418 fin1aufil 23849 rectbntr0 24761 lgam1 27009 gam1 27010 konigsberg 30080 ex-po 30258 strlem1 32073 eulerpartlemt 33991 nalfal 35887 bj-mt2bi 36044 finxpreclem3 36872 |
Copyright terms: Public domain | W3C validator |