![]() |
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 248 | . 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 7819 omopthlem2 8607 fineqv 9208 nd3 10526 axunndlem1 10532 axregndlem1 10539 axregndlem2 10540 axregnd 10541 axacndlem5 10548 canthp1lem2 10590 alephgch 10611 inatsk 10715 addnidpi 10838 indpi 10844 archnq 10917 fsumsplit 15627 sumsplit 15654 geoisum1c 15766 fprodm1 15851 m1dvdsndvds 16671 gexdvds 19367 chtub 26563 nolt02o 27046 nogt01o 27047 wlkp1lem6 28629 avril1 29410 ballotlemi1 33105 ballotlemii 33106 distel 34381 onsucsuccmpi 34918 bj-inftyexpitaudisj 35679 bj-inftyexpidisj 35684 poimirlem28 36109 poimirlem32 36113 n0eldmqseq 37114 lcmineqlem23 40511 nvelim 45362 0nodd 46111 2nodd 46113 |
Copyright terms: Public domain | W3C validator |