![]() |
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 4351 vnex 5320 opthwiener 5524 epelg 5590 harndom 9600 alephprc 10137 unialeph 10139 ndvdsi 16446 nprmi 16723 dec2dvds 17097 dec5dvds2 17099 mreexmrid 17688 sinhalfpilem 26520 ppi2i 27227 axlowdimlem13 28984 ex-mod 30478 measvuni 34195 ballotlem2 34470 sgnmulsgp 34532 bnj1224 34794 bnj1541 34849 bnj1311 35017 dfon2lem7 35771 onsucsuccmpi 36426 bj-imn3ani 36570 sbn1ALT 36841 bj-0nelmpt 37099 bj-pinftynminfty 37210 poimirlem30 37637 clsk1indlem4 44034 alimp-no-surprise 49012 |
Copyright terms: Public domain | W3C validator |