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 8708 fin1a2s 9838 gchinf 10081 pwfseqlem4 10086 pcfac 16237 prmreclem3 16256 sylow1lem1 18725 irredrmul 19459 mdetunilem9 21231 ioorcl2 24175 itg2gt0 24363 mdegmullem 24674 atom1d 30132 rr-phpd 40569 notnotrALT 40870 fourierdlem79 42477 |
Copyright terms: Public domain | W3C validator |