![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mt2d | Structured version Visualization version GIF version |
Description: Modus tollens deduction. (Contributed by NM, 4-Jul-1994.) |
Ref | Expression |
---|---|
mt2d.1 | ⊢ (𝜑 → 𝜒) |
mt2d.2 | ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) |
Ref | Expression |
---|---|
mt2d | ⊢ (𝜑 → ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mt2d.1 | . 2 ⊢ (𝜑 → 𝜒) | |
2 | mt2d.2 | . . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) | |
3 | 2 | con2d 134 | . 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: mt2i 137 nsyl3 138 tz7.44-3 8414 sdomdomtr 9116 domsdomtr 9118 infdif 10210 ackbij1b 10240 isf32lem5 10358 alephreg 10583 cfpwsdom 10585 inar1 10776 tskcard 10782 npomex 10997 recnz 12644 rpnnen1lem5 12972 fznuz 13590 uznfz 13591 seqcoll2 14433 ramub1lem1 16966 pgpfac1lem1 19992 lsppratlem6 20999 nconnsubb 23247 iunconnlem 23251 clsconn 23254 xkohaus 23477 reconnlem1 24662 ivthlem2 25301 perfectlem1 27075 lgseisenlem1 27221 ex-natded5.8-2 30100 oddpwdc 33817 erdszelem9 34654 relowlpssretop 36709 sucneqond 36710 heiborlem8 37150 lcvntr 38360 ncvr1 38606 llnneat 38849 2atnelpln 38879 lplnneat 38880 lplnnelln 38881 3atnelvolN 38921 lvolneatN 38923 lvolnelln 38924 lvolnelpln 38925 lplncvrlvol 38951 4atexlemntlpq 39403 cdleme0nex 39625 nlimsuc 42655 |
Copyright terms: Public domain | W3C validator |