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  5256  opthwiener  5459  epelg  5522  harndom  9457  alephprc  9999  unialeph  10001  ndvdsi  16327  nprmi  16604  dec2dvds  16979  dec5dvds2  16981  mreexmrid  17553  sinhalfpilem  26402  ppi2i  27109  axlowdimlem13  28936  ex-mod  30433  sgnmulsgp  32833  measvuni  34250  ballotlem2  34525  bnj1224  34836  bnj1541  34891  bnj1311  35059  dfon2lem7  35854  onsucsuccmpi  36510  bj-imn3ani  36654  sbn1ALT  36925  bj-0nelmpt  37183  bj-pinftynminfty  37294  poimirlem30  37713  clsk1indlem4  44164  tannpoly  47017  alimp-no-surprise  49909