Theorem mtbi 321

Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mtbi.1	⊢ ¬ 𝜑
mtbi.2	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mtbi	⊢ ¬ 𝜓

Proof of Theorem mtbi

Step	Hyp	Ref	Expression
1		mtbi.1	. 2 ⊢ ¬ 𝜑
2		mtbi.2	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpri 227	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	mto 196	1 ⊢ ¬ 𝜓

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  4337  vnex  5313  opthwiener  5513  epelg  5580  harndom  9553  alephprc  10090  unialeph  10092  ndvdsi  16351  nprmi  16622  dec2dvds  16992  dec5dvds2  16994  mreexmrid  17583  sinhalfpilem  25964  ppi2i  26662  axlowdimlem13  28201  ex-mod  29691  measvuni  33200  ballotlem2  33475  sgnmulsgp  33537  bnj1224  33800  bnj1541  33855  bnj1311  34023  dfon2lem7  34749  onsucsuccmpi  35316  bj-imn3ani  35453  sbn1ALT  35725  bj-0nelmpt  35985  bj-pinftynminfty  36096  poimirlem30  36506  clsk1indlem4  42780  alimp-no-surprise  47781