|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > mtbi | Structured version Visualization version GIF version | ||
| Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) | 
| Ref | Expression | 
|---|---|
| mtbi.1 | ⊢ ¬ 𝜑 | 
| mtbi.2 | ⊢ (𝜑 ↔ 𝜓) | 
| Ref | Expression | 
|---|---|
| mtbi | ⊢ ¬ 𝜓 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | mtbi.1 | . 2 ⊢ ¬ 𝜑 | |
| 2 | mtbi.2 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 3 | 2 | biimpri 228 | . 2 ⊢ (𝜓 → 𝜑) | 
| 4 | 1, 3 | mto 197 | 1 ⊢ ¬ 𝜓 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ 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: mtbir 323 vn0 4344 vnex 5313 opthwiener 5518 epelg 5584 harndom 9603 alephprc 10140 unialeph 10142 ndvdsi 16450 nprmi 16727 dec2dvds 17102 dec5dvds2 17104 mreexmrid 17687 sinhalfpilem 26506 ppi2i 27213 axlowdimlem13 28970 ex-mod 30469 measvuni 34216 ballotlem2 34492 sgnmulsgp 34554 bnj1224 34816 bnj1541 34871 bnj1311 35039 dfon2lem7 35791 onsucsuccmpi 36445 bj-imn3ani 36589 sbn1ALT 36860 bj-0nelmpt 37118 bj-pinftynminfty 37229 poimirlem30 37658 clsk1indlem4 44062 alimp-no-surprise 49355 | 
| Copyright terms: Public domain | W3C validator |