Theorem mtbi 310

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 216	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	mto 186	1 ⊢ ¬ 𝜓

Syntax hints:  ¬ wn 3   ↔ wb 194

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 195

This theorem is referenced by:  mtbir  311  vprc  4719  vnex  4721  opthwiener  4892  harndom  8329  alephprc  8782  unialeph  8784  ndvdsi  14920  bitsfzo  14941  nprmi  15186  dec2dvds  15551  dec5dvds2  15553  mreexmrid  16072  sinhalfpilem  23936  ppi2i  24612  axlowdimlem13  25552  ex-mod  26464  measvuni  29410  ballotlem2  29683  sgnmulsgp  29745  bnj1224  29932  bnj1541  29986  bnj1311  30152  dfon2lem7  30744  onsucsuccmpi  31418  bj-imn3ani  31551  bj-0nelmpt  32046  bj-pinftynminfty  32087  poimirlem30  32405  clsk1indlem4  37158  alimp-no-surprise  42292