![]() |
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 142 | . 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 144 nsyl2 145 ecase23d 1601 disjss3 4874 nnsuc 7348 unxpdomlem2 8440 oismo 8721 cnfcom3lem 8884 rankelb 8971 fin33i 9513 isf34lem4 9521 canthp1lem2 9797 gchcda1 9800 pwfseqlem3 9804 inttsk 9918 r1tskina 9926 nqereu 10073 zbtwnre 12076 discr1 13301 seqcoll2 13545 bitsfzo 15537 bitsf1 15548 eucalglt 15678 4sqlem17 16043 4sqlem18 16044 ramubcl 16100 psgnunilem5 18271 psgnunilem5OLD 18272 odnncl 18322 gexnnod 18361 sylow1lem1 18371 torsubg 18617 prmcyg 18655 ablfacrplem 18825 pgpfac1lem2 18835 pgpfac1lem3a 18836 pgpfac1lem3 18837 xrsdsreclblem 20159 prmirredlem 20208 ppttop 21189 pptbas 21190 regr1lem 21920 alexsublem 22225 reconnlem1 23006 metnrmlem1a 23038 vitalilem4 23784 vitalilem5 23785 itg2gt0 23933 rollelem 24158 lhop1lem 24182 coefv0 24410 plyexmo 24474 lgamucov 25184 ppinprm 25298 chtnprm 25300 lgsdir 25477 lgseisenlem1 25520 2sqlem7 25569 2sqblem 25576 pntpbnd1 25695 dfon2lem8 32228 poimirlem25 33973 fdc 34078 ac6s6 34516 2atm 35597 llnmlplnN 35609 trlval3 36257 cdleme0moN 36295 cdleme18c 36363 qirropth 38311 aacllem 43453 |
Copyright terms: Public domain | W3C validator |