![]() |
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 9155 phpeqdOLD 9165 fin1a2s 10346 gchinf 10589 pwfseqlem4 10594 pcfac 16763 prmreclem3 16782 sylow1lem1 19371 irredrmul 20121 mdetunilem9 21953 ioorcl2 24920 itg2gt0 25109 mdegmullem 25427 atom1d 31181 rr-phpd 42425 notnotrALT 42753 fourierdlem79 44358 |
Copyright terms: Public domain | W3C validator |