|   | 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 7904 omopthlem2 8699 fineqv 9300 nd3 10630 axunndlem1 10636 axregndlem1 10643 axregndlem2 10644 axregnd 10645 axacndlem5 10652 canthp1lem2 10694 alephgch 10715 inatsk 10819 addnidpi 10942 indpi 10948 archnq 11021 fsumsplit 15778 sumsplit 15805 geoisum1c 15917 fprodm1 16004 m1dvdsndvds 16837 gexdvds 19603 chtub 27257 nolt02o 27741 nogt01o 27742 wlkp1lem6 29697 avril1 30483 ballotlemi1 34506 ballotlemii 34507 distel 35805 onsucsuccmpi 36445 bj-inftyexpitaudisj 37207 bj-inftyexpidisj 37212 poimirlem28 37656 poimirlem32 37660 n0eldmqseq 38651 lcmineqlem23 42053 nvelim 47140 0nodd 48091 2nodd 48093 | 
| Copyright terms: Public domain | W3C validator |