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 128 | . 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 131 nsyl3 132 tz7.44-3 7391 sdomdomtr 7978 domsdomtr 7980 infdif 8914 ackbij1b 8944 isf32lem5 9062 alephreg 9283 cfpwsdom 9285 inar1 9476 tskcard 9482 npomex 9697 recnz 11328 rpnnen1lem5 11694 rpnnen1lem5OLD 11700 fznuz 12291 uznfz 12292 seqcoll2 13106 ramub1lem1 15568 pgpfac1lem1 18296 lsppratlem6 18973 nconsubb 21036 iunconlem 21040 clscon 21043 xkohaus 21266 reconnlem1 22437 ivthlem2 23028 perfectlem1 24754 lgseisenlem1 24900 ex-natded5.8-2 26663 oddpwdc 29743 erdszelem9 30435 relowlpssretop 32388 sucneqond 32389 heiborlem8 32787 lcvntr 33331 ncvr1 33577 llnneat 33818 2atnelpln 33848 lplnneat 33849 lplnnelln 33850 3atnelvolN 33890 lvolneatN 33892 lvolnelln 33893 lvolnelpln 33894 lplncvrlvol 33920 4atexlemntlpq 34372 cdleme0nex 34595 |
Copyright terms: Public domain | W3C validator |