| 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 4293 vnex 5250 opthwiener 5452 epelg 5515 harndom 9443 alephprc 9982 unialeph 9984 ndvdsi 16315 nprmi 16592 dec2dvds 16967 dec5dvds2 16969 mreexmrid 17541 sinhalfpilem 26392 ppi2i 27099 axlowdimlem13 28925 ex-mod 30419 sgnmulsgp 32816 measvuni 34217 ballotlem2 34492 bnj1224 34803 bnj1541 34858 bnj1311 35026 dfon2lem7 35802 onsucsuccmpi 36456 bj-imn3ani 36600 sbn1ALT 36871 bj-0nelmpt 37129 bj-pinftynminfty 37240 poimirlem30 37669 clsk1indlem4 44056 tannpoly 46900 alimp-no-surprise 49792 |
| Copyright terms: Public domain | W3C validator |