![]() |
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 247 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
4 | 1, 3 | mtoi 198 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: limom 7884 omopthlem2 8682 fineqv 9290 nd3 10623 axunndlem1 10629 axregndlem1 10636 axregndlem2 10637 axregnd 10638 axacndlem5 10645 canthp1lem2 10687 alephgch 10708 inatsk 10812 addnidpi 10935 indpi 10941 archnq 11014 fsumsplit 15740 sumsplit 15767 geoisum1c 15879 fprodm1 15964 m1dvdsndvds 16795 gexdvds 19578 chtub 27238 nolt02o 27722 nogt01o 27723 wlkp1lem6 29612 avril1 30393 ballotlemi1 34349 ballotlemii 34350 distel 35640 onsucsuccmpi 36168 bj-inftyexpitaudisj 36925 bj-inftyexpidisj 36930 poimirlem28 37362 poimirlem32 37366 n0eldmqseq 38360 lcmineqlem23 41763 nvelim 46772 0nodd 47583 2nodd 47585 |
Copyright terms: Public domain | W3C validator |