|   | 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 9253 phpeqdOLD 9263 fin1a2s 10455 gchinf 10698 pwfseqlem4 10703 pcfac 16938 prmreclem3 16957 sylow1lem1 19617 irredrmul 20428 mdetunilem9 22627 ioorcl2 25608 itg2gt0 25796 mdegmullem 26118 atom1d 32373 rr-phpd 44227 notnotrALT 44554 fourierdlem79 46205 | 
| Copyright terms: Public domain | W3C validator |