|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > mt3d | Structured version Visualization version GIF version | ||
| Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.) | 
| Ref | Expression | 
|---|---|
| mt3d.1 | ⊢ (𝜑 → ¬ 𝜒) | 
| mt3d.2 | ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) | 
| Ref | Expression | 
|---|---|
| mt3d | ⊢ (𝜑 → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | mt3d.1 | . 2 ⊢ (𝜑 → ¬ 𝜒) | |
| 2 | mt3d.2 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) | |
| 3 | 2 | con1d 145 | . 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: mt3i 149 olcnd 877 ecase23d 1474 disjss3 5141 nnsuc 7906 poxp2 8169 frrlem14 8325 unxpdomlem2 9288 oismo 9581 cnfcom3lem 9744 rankelb 9865 fin33i 10410 isf34lem4 10418 canthp1lem2 10694 gchdju1 10697 pwfseqlem3 10701 inttsk 10815 r1tskina 10823 nqereu 10970 zbtwnre 12989 discr1 14279 seqcoll2 14505 bitsfzo 16473 bitsf1 16484 eucalglt 16623 4sqlem17 17000 4sqlem18 17001 ramubcl 17057 psgnunilem5 19513 odnncl 19564 gexnnod 19607 sylow1lem1 19617 torsubg 19873 prmcyg 19913 ablfacrplem 20086 pgpfac1lem2 20096 pgpfac1lem3a 20097 pgpfac1lem3 20098 xrsdsreclblem 21431 prmirredlem 21484 ppttop 23015 pptbas 23016 regr1lem 23748 alexsublem 24053 reconnlem1 24849 metnrmlem1a 24881 vitalilem4 25647 vitalilem5 25648 itg2gt0 25796 rollelem 26028 lhop1lem 26053 coefv0 26288 plyexmo 26356 lgamucov 27082 ppinprm 27196 chtnprm 27198 lgsdir 27377 lgseisenlem1 27420 2sqlem7 27469 2sqblem 27476 pntpbnd1 27631 madebdaylemlrcut 27938 dfon2lem8 35792 poimirlem25 37653 fdc 37753 ac6s6 38180 2atm 39530 llnmlplnN 39542 trlval3 40190 cdleme0moN 40228 cdleme18c 40296 qirropth 42924 aacllem 49375 | 
| Copyright terms: Public domain | W3C validator |