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 229 | . 2 ⊢ (𝜓 → 𝜑) |
4 | 1, 3 | mto 198 | 1 ⊢ ¬ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 |
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 208 |
This theorem is referenced by: mtbir 324 vnex 5209 opthwiener 5395 epelg 5459 harndom 9016 alephprc 9513 unialeph 9515 ndvdsi 15751 nprmi 16021 dec2dvds 16387 dec5dvds2 16389 mreexmrid 16902 sinhalfpilem 24976 ppi2i 25673 axlowdimlem13 26667 ex-mod 28155 measvuni 31372 ballotlem2 31645 sgnmulsgp 31707 bnj1224 31972 bnj1541 32027 bnj1311 32193 dfon2lem7 32931 onsucsuccmpi 33688 bj-imn3ani 33818 bj-0nelmpt 34300 bj-pinftynminfty 34401 poimirlem30 34803 clsk1indlem4 40272 alimp-no-surprise 44810 |
Copyright terms: Public domain | W3C validator |