![]() |
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 218 | . 2 ⊢ (𝜓 → 𝜑) |
4 | 1, 3 | mto 188 | 1 ⊢ ¬ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 |
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 197 |
This theorem is referenced by: mtbir 312 vprc 4948 vnex 4950 opthwiener 5124 harndom 8636 alephprc 9132 unialeph 9134 ndvdsi 15358 bitsfzo 15379 nprmi 15624 dec2dvds 15989 dec5dvds2 15991 mreexmrid 16525 sinhalfpilem 24435 ppi2i 25115 axlowdimlem13 26054 ex-mod 27638 measvuni 30607 ballotlem2 30880 sgnmulsgp 30942 bnj1224 31200 bnj1541 31254 bnj1311 31420 dfon2lem7 32020 onsucsuccmpi 32769 bj-imn3ani 32900 bj-0nelmpt 33393 bj-pinftynminfty 33443 poimirlem30 33770 clsk1indlem4 38862 alimp-no-surprise 43058 |
Copyright terms: Public domain | W3C validator |