Theorem mtbi 311

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

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  4829  vnex  4831  opthwiener  5005  harndom  8510  alephprc  8960  unialeph  8962  ndvdsi  15183  bitsfzo  15204  nprmi  15449  dec2dvds  15814  dec5dvds2  15816  mreexmrid  16350  sinhalfpilem  24260  ppi2i  24940  axlowdimlem13  25879  ex-mod  27436  measvuni  30405  ballotlem2  30678  sgnmulsgp  30740  bnj1224  30998  bnj1541  31052  bnj1311  31218  dfon2lem7  31818  onsucsuccmpi  32567  bj-imn3ani  32697  bj-0nelmpt  33194  bj-pinftynminfty  33244  poimirlem30  33569  clsk1indlem4  38659  alimp-no-surprise  42855