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  vn0  4325  vnex  5289  opthwiener  5494  epelg  5559  harndom  9581  alephprc  10118  unialeph  10120  ndvdsi  16436  nprmi  16713  dec2dvds  17088  dec5dvds2  17090  mreexmrid  17660  sinhalfpilem  26429  ppi2i  27136  axlowdimlem13  28938  ex-mod  30435  sgnmulsgp  32827  measvuni  34250  ballotlem2  34526  bnj1224  34837  bnj1541  34892  bnj1311  35060  dfon2lem7  35812  onsucsuccmpi  36466  bj-imn3ani  36610  sbn1ALT  36881  bj-0nelmpt  37139  bj-pinftynminfty  37250  poimirlem30  37679  clsk1indlem4  44035  alimp-no-surprise  49612