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 138 | . 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 140 nsyl2 141 ecase23d 1428 disjss3 4582 nnsuc 6974 unxpdomlem2 8050 oismo 8328 cnfcom3lem 8483 rankelb 8570 fin33i 9074 isf34lem4 9082 canthp1lem2 9354 gchcda1 9357 pwfseqlem3 9361 inttsk 9475 r1tskina 9483 nqereu 9630 zbtwnre 11662 discr1 12862 seqcoll2 13106 bitsfzo 14995 bitsf1 15006 eucalglt 15136 4sqlem17 15503 4sqlem18 15504 ramubcl 15560 psgnunilem5 17737 odnncl 17787 gexnnod 17826 sylow1lem1 17836 torsubg 18080 prmcyg 18118 ablfacrplem 18287 pgpfac1lem2 18297 pgpfac1lem3a 18298 pgpfac1lem3 18299 xrsdsreclblem 19611 prmirredlem 19660 ppttop 20621 pptbas 20622 regr1lem 21352 alexsublem 21658 reconnlem1 22437 metnrmlem1a 22469 vitalilem4 23186 vitalilem5 23187 itg2gt0 23333 rollelem 23556 lhop1lem 23580 coefv0 23808 plyexmo 23872 lgamucov 24564 ppinprm 24678 chtnprm 24680 lgsdir 24857 lgseisenlem1 24900 2sqlem7 24949 2sqblem 24956 pntpbnd1 25075 dfon2lem8 30939 nobndup 31099 nobnddown 31100 nofulllem5 31105 poimirlem25 32604 fdc 32711 ac6s6 33150 2atm 33831 llnmlplnN 33843 trlval3 34492 cdleme0moN 34530 cdleme18c 34598 qirropth 36491 aacllem 42356 |
Copyright terms: Public domain | W3C validator |