Theorem mtbi 325

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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  mtbir  326  vnexOLD  5282  opthwiener  5499  epelg  5564  harndom  9525  alephprc  10084  unialeph  10086  ndvdsi  16471  nprmi  16748  dec2dvds  17124  dec5dvds2  17126  mreexmrid  17700  sinhalfpilem  26609  ppi2i  27314  axlowdimlem13  29285  ex-mod  30781  sgnmulsgp  33157  measvuni  34585  ballotlem2  34860  bnj1224  35170  bnj1541  35225  bnj1311  35393  dfon2lem7  36260  onsucsuccmpi  36935  bj-imn3ani  37161  sbn1ALT  37474  bj-0nelmpt  37739  bj-pinftynminfty  37852  poimirlem30  38282  clsk1indlem4  44753  tannpoly  47610  alimp-no-surprise  50542