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  4948  vnex  4950  opthwiener  5124  harndom  8636  alephprc  9132  unialeph  9134  ndvdsi  15358  bitsfzo  15379  nprmi  15624  dec2dvds  15989  dec5dvds2  15991  mreexmrid  16525  sinhalfpilem  24435  ppi2i  25115  axlowdimlem13  26054  ex-mod  27638  measvuni  30607  ballotlem2  30880  sgnmulsgp  30942  bnj1224  31200  bnj1541  31254  bnj1311  31420  dfon2lem7  32020  onsucsuccmpi  32769  bj-imn3ani  32900  bj-0nelmpt  33393  bj-pinftynminfty  33443  poimirlem30  33770  clsk1indlem4  38862  alimp-no-surprise  43058