![]() |
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 240 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
4 | 1, 3 | mtoi 191 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: limom 7312 omopthlem2 7974 fineqv 8415 dfac2OLD 9239 nd3 9697 axunndlem1 9703 axregndlem1 9710 axregndlem2 9711 axregnd 9712 axacndlem5 9719 canthp1lem2 9761 alephgch 9782 inatsk 9886 addnidpi 10009 indpi 10015 archnq 10088 fsumsplit 14809 sumsplit 14835 geoisum1c 14946 fprodm1 15031 m1dvdsndvds 15833 gexdvds 18309 chtub 25286 wlkp1lem6 26923 avril1 27839 ballotlemi1 31073 ballotlemii 31074 distel 32213 nolt02o 32350 onsucsuccmpi 32942 bj-inftyexpidisj 33588 poimirlem28 33918 poimirlem32 33922 nvelim 41965 0nodd 42597 2nodd 42599 |
Copyright terms: Public domain | W3C validator |