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 ⊢ ¬ 𝜓

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mtbir  326  vnexOLD  5278  opthwiener  5494  epelg  5559  harndom  9593  alephprc  10217  unialeph  10219  ndvdsi  16626  nprmi  16908  dec2dvds  17285  dec5dvds2  17287  mreexmrid  17867  sinhalfpilem  26849  ppi2i  27553  axlowdimlem13  29589  ex-mod  31107  sgnmulsgp  33519  measvuni  34958  ballotlem2  35232  bnj1224  35542  bnj1541  35597  bnj1311  35765  mirimanofffr  36670  dfon2lem7  36766  onsucsuccmpi  37446  bj-imn3ani  37672  sbn1ALT  37985  bj-0nelmpt  38308  bj-pinftynminfty  38416  poimirlem30  38836  clsk1indlem4  45305  tannpoly  48213  alimp-no-surprise  51305