![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mt4d | Structured version Visualization version GIF version |
Description: Modus tollens deduction. Deduction form of mt4 116. (Contributed by NM, 9-Jun-2006.) |
Ref | Expression |
---|---|
mt4d.1 | ⊢ (𝜑 → 𝜓) |
mt4d.2 | ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
Ref | Expression |
---|---|
mt4d | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mt4d.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | mt4d.2 | . . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) | |
3 | 2 | con4d 115 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1, 3 | mpd 15 | 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: mt4i 118 pm2.18d 127 phpeqd 9215 phpeqdOLD 9225 fin1a2s 10409 gchinf 10652 pwfseqlem4 10657 pcfac 16832 prmreclem3 16851 sylow1lem1 19466 irredrmul 20241 mdetunilem9 22122 ioorcl2 25089 itg2gt0 25278 mdegmullem 25596 atom1d 31606 rr-phpd 42962 notnotrALT 43290 fourierdlem79 44901 |
Copyright terms: Public domain | W3C validator |