![]() |
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 227 | . 2 ⊢ (𝜓 → 𝜑) |
4 | 1, 3 | mto 196 | 1 ⊢ ¬ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ 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: mtbir 322 vn0 4341 vnex 5319 opthwiener 5520 epelg 5587 harndom 9605 alephprc 10142 unialeph 10144 ndvdsi 16414 nprmi 16690 dec2dvds 17065 dec5dvds2 17067 mreexmrid 17656 sinhalfpilem 26491 ppi2i 27197 axlowdimlem13 28888 ex-mod 30382 measvuni 34047 ballotlem2 34322 sgnmulsgp 34384 bnj1224 34646 bnj1541 34701 bnj1311 34869 dfon2lem7 35613 onsucsuccmpi 36155 bj-imn3ani 36292 sbn1ALT 36563 bj-0nelmpt 36823 bj-pinftynminfty 36934 poimirlem30 37351 clsk1indlem4 43711 alimp-no-surprise 48529 |
Copyright terms: Public domain | W3C validator |