Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mtbii | Structured version Visualization version GIF version |
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.) |
Ref | Expression |
---|---|
mtbii.min | ⊢ ¬ 𝜓 |
mtbii.maj | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
mtbii | ⊢ (𝜑 → ¬ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbii.min | . 2 ⊢ ¬ 𝜓 | |
2 | mtbii.maj | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 2 | biimprd 237 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
4 | 1, 3 | mtoi 189 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: limom 6972 omopthlem2 7623 fineqv 8060 dfac2 8836 nd3 9290 axunndlem1 9296 axregndlem1 9303 axregndlem2 9304 axregnd 9305 axacndlem5 9312 canthp1lem2 9354 alephgch 9375 inatsk 9479 addnidpi 9602 indpi 9608 archnq 9681 fsumsplit 14318 sumsplit 14341 geoisum1c 14450 fprodm1 14536 m1dvdsndvds 15341 gexdvds 17822 chtub 24737 avril1 26711 ballotlemi1 29891 ballotlemii 29892 distel 30953 fvnobday 31081 onsucsuccmpi 31612 bj-inftyexpidisj 32274 poimirlem28 32607 poimirlem32 32611 nvelim 39849 1wlkp1lem6 40887 0nodd 41600 2nodd 41602 |
Copyright terms: Public domain | W3C validator |