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 4285 vnex 5258 opthwiener 5458 epelg 5525 harndom 9419 alephprc 9956 unialeph 9958 ndvdsi 16220 nprmi 16491 dec2dvds 16861 dec5dvds2 16863 mreexmrid 17449 sinhalfpilem 25726 ppi2i 26424 axlowdimlem13 27611 ex-mod 29101 measvuni 32480 ballotlem2 32755 sgnmulsgp 32817 bnj1224 33080 bnj1541 33135 bnj1311 33303 dfon2lem7 34048 onsucsuccmpi 34728 bj-imn3ani 34865 sbn1ALT 35137 bj-0nelmpt 35392 bj-pinftynminfty 35503 poimirlem30 35912 clsk1indlem4 41975 alimp-no-surprise 46836 |
Copyright terms: Public domain | W3C validator |