![]() |
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 132 | . 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 135 nsyl3 136 tz7.44-3 7775 sdomdomtr 8368 domsdomtr 8370 infdif 9353 ackbij1b 9383 isf32lem5 9501 alephreg 9726 cfpwsdom 9728 inar1 9919 tskcard 9925 npomex 10140 recnz 11787 rpnnen1lem5 12110 fznuz 12723 uznfz 12724 seqcoll2 13545 ramub1lem1 16108 pgpfac1lem1 18834 lsppratlem6 19520 nconnsubb 21604 iunconnlem 21608 clsconn 21611 xkohaus 21834 reconnlem1 23006 ivthlem2 23625 perfectlem1 25374 lgseisenlem1 25520 ex-natded5.8-2 27825 oddpwdc 30957 erdszelem9 31723 relowlpssretop 33752 sucneqond 33753 heiborlem8 34154 lcvntr 35096 ncvr1 35342 llnneat 35584 2atnelpln 35614 lplnneat 35615 lplnnelln 35616 3atnelvolN 35656 lvolneatN 35658 lvolnelln 35659 lvolnelpln 35660 lplncvrlvol 35686 4atexlemntlpq 36138 cdleme0nex 36360 |
Copyright terms: Public domain | W3C validator |