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  5272  opthwiener  5487  epelg  5552  harndom  9512  alephprc  10071  unialeph  10073  ndvdsi  16458  nprmi  16735  dec2dvds  17111  dec5dvds2  17113  mreexmrid  17687  sinhalfpilem  26582  ppi2i  27287  axlowdimlem13  29209  ex-mod  30705  sgnmulsgp  33084  measvuni  34516  ballotlem2  34791  bnj1224  35101  bnj1541  35156  bnj1311  35324  dfon2lem7  36145  onsucsuccmpi  36811  bj-imn3ani  37037  sbn1ALT  37350  bj-0nelmpt  37613  bj-pinftynminfty  37726  poimirlem30  38156  clsk1indlem4  44627  tannpoly  47483  alimp-no-surprise  50411