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 8813 fin1a2s 9993 gchinf 10236 pwfseqlem4 10241 pcfac 16415 prmreclem3 16434 sylow1lem1 18941 irredrmul 19679 mdetunilem9 21471 ioorcl2 24423 itg2gt0 24612 mdegmullem 24930 atom1d 30388 rr-phpd 41440 notnotrALT 41763 fourierdlem79 43344 |
Copyright terms: Public domain | W3C validator |