Theorem mtbi 322

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

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  4293  vnex  5250  opthwiener  5452  epelg  5515  harndom  9443  alephprc  9982  unialeph  9984  ndvdsi  16315  nprmi  16592  dec2dvds  16967  dec5dvds2  16969  mreexmrid  17541  sinhalfpilem  26392  ppi2i  27099  axlowdimlem13  28925  ex-mod  30419  sgnmulsgp  32816  measvuni  34217  ballotlem2  34492  bnj1224  34803  bnj1541  34858  bnj1311  35026  dfon2lem7  35802  onsucsuccmpi  36456  bj-imn3ani  36600  sbn1ALT  36871  bj-0nelmpt  37129  bj-pinftynminfty  37240  poimirlem30  37669  clsk1indlem4  44056  tannpoly  46900  alimp-no-surprise  49792