![]() |
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 145 | . 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 149 olcnd 875 ecase23d 1469 disjss3 5148 nnsuc 7889 poxp2 8148 frrlem14 8305 unxpdomlem2 9276 oismo 9565 cnfcom3lem 9728 rankelb 9849 fin33i 10394 isf34lem4 10402 canthp1lem2 10678 gchdju1 10681 pwfseqlem3 10685 inttsk 10799 r1tskina 10807 nqereu 10954 zbtwnre 12963 discr1 14237 seqcoll2 14462 bitsfzo 16413 bitsf1 16424 eucalglt 16559 4sqlem17 16933 4sqlem18 16934 ramubcl 16990 psgnunilem5 19461 odnncl 19512 gexnnod 19555 sylow1lem1 19565 torsubg 19821 prmcyg 19861 ablfacrplem 20034 pgpfac1lem2 20044 pgpfac1lem3a 20045 pgpfac1lem3 20046 xrsdsreclblem 21362 prmirredlem 21415 ppttop 22954 pptbas 22955 regr1lem 23687 alexsublem 23992 reconnlem1 24786 metnrmlem1a 24818 vitalilem4 25584 vitalilem5 25585 itg2gt0 25734 rollelem 25965 lhop1lem 25990 coefv0 26227 plyexmo 26293 lgamucov 27015 ppinprm 27129 chtnprm 27131 lgsdir 27310 lgseisenlem1 27353 2sqlem7 27402 2sqblem 27409 pntpbnd1 27564 madebdaylemlrcut 27871 dfon2lem8 35517 poimirlem25 37249 fdc 37349 ac6s6 37776 2atm 39130 llnmlplnN 39142 trlval3 39790 cdleme0moN 39828 cdleme18c 39896 qirropth 42470 aacllem 48420 |
Copyright terms: Public domain | W3C validator |