Theorem mtbi 311

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

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  mtbir  312  vprc  4724  vnex  4726  opthwiener  4901  harndom  8352  alephprc  8805  unialeph  8807  ndvdsi  14974  bitsfzo  14995  nprmi  15240  dec2dvds  15605  dec5dvds2  15607  mreexmrid  16126  sinhalfpilem  24019  ppi2i  24695  axlowdimlem13  25634  ex-mod  26698  measvuni  29604  ballotlem2  29877  sgnmulsgp  29939  bnj1224  30126  bnj1541  30180  bnj1311  30346  dfon2lem7  30938  onsucsuccmpi  31612  bj-imn3ani  31745  bj-0nelmpt  32250  bj-pinftynminfty  32291  poimirlem30  32609  clsk1indlem4  37362  alimp-no-surprise  42336