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  vnex  5261  opthwiener  5470  epelg  5533  harndom  9479  alephprc  10021  unialeph  10023  ndvdsi  16351  nprmi  16628  dec2dvds  17003  dec5dvds2  17005  mreexmrid  17578  sinhalfpilem  26440  ppi2i  27147  axlowdimlem13  29039  ex-mod  30536  sgnmulsgp  32934  measvuni  34391  ballotlem2  34666  bnj1224  34976  bnj1541  35031  bnj1311  35199  dfon2lem7  36000  onsucsuccmpi  36656  bj-imn3ani  36809  sbn1ALT  37103  bj-0nelmpt  37366  bj-pinftynminfty  37479  poimirlem30  37898  clsk1indlem4  44397  tannpoly  47247  alimp-no-surprise  50137