Theorem mtbi 321

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  mtbir  322  vn0  4277  vnex  5241  opthwiener  5430  epelg  5495  harndom  9282  alephprc  9839  unialeph  9841  ndvdsi  16102  nprmi  16375  dec2dvds  16745  dec5dvds2  16747  mreexmrid  17333  sinhalfpilem  25601  ppi2i  26299  axlowdimlem13  27303  ex-mod  28792  measvuni  32161  ballotlem2  32434  sgnmulsgp  32496  bnj1224  32760  bnj1541  32815  bnj1311  32983  dfon2lem7  33744  onsucsuccmpi  34611  bj-imn3ani  34748  sbn1ALT  35021  bj-0nelmpt  35266  bj-pinftynminfty  35377  poimirlem30  35786  clsk1indlem4  41607  alimp-no-surprise  46437