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 136 | . 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 139 nsyl3 140 tz7.44-3 8033 sdomdomtr 8638 domsdomtr 8640 infdif 9619 ackbij1b 9649 isf32lem5 9767 alephreg 9992 cfpwsdom 9994 inar1 10185 tskcard 10191 npomex 10406 recnz 12045 rpnnen1lem5 12368 fznuz 12977 uznfz 12978 seqcoll2 13811 ramub1lem1 16350 pgpfac1lem1 19125 lsppratlem6 19853 nconnsubb 21959 iunconnlem 21963 clsconn 21966 xkohaus 22189 reconnlem1 23361 ivthlem2 23980 perfectlem1 25732 lgseisenlem1 25878 ex-natded5.8-2 28120 oddpwdc 31511 erdszelem9 32343 relowlpssretop 34527 sucneqond 34528 heiborlem8 34977 lcvntr 36042 ncvr1 36288 llnneat 36530 2atnelpln 36560 lplnneat 36561 lplnnelln 36562 3atnelvolN 36602 lvolneatN 36604 lvolnelln 36605 lvolnelpln 36606 lplncvrlvol 36632 4atexlemntlpq 37084 cdleme0nex 37306 |
Copyright terms: Public domain | W3C validator |