| 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 199 | 1 ⊢ (𝜑 → ¬ 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: limom 7822 omopthlem2 8585 fineqv 9168 nelaneq 9512 nd3 10502 axunndlem1 10508 axregndlem1 10515 axregndlem2 10516 axregnd 10517 axacndlem5 10524 canthp1lem2 10566 alephgch 10587 inatsk 10691 addnidpi 10814 indpi 10820 archnq 10893 fsumsplit 15667 sumsplit 15694 geoisum1c 15806 fprodm1 15893 m1dvdsndvds 16729 gexdvds 19482 chtub 27140 nolt02o 27624 nogt01o 27625 wlkp1lem6 29641 avril1 30426 ballotlemi1 34490 ballotlemii 34491 onvf1odlem1 35095 distel 35796 onsucsuccmpi 36436 bj-inftyexpitaudisj 37198 bj-inftyexpidisj 37203 poimirlem28 37647 poimirlem32 37651 n0eldmqseq 38646 lcmineqlem23 42044 nvelim 47127 0nodd 48174 2nodd 48176 |
| Copyright terms: Public domain | W3C validator |