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  4368  vnex  5332  opthwiener  5533  epelg  5600  harndom  9631  alephprc  10168  unialeph  10170  ndvdsi  16460  nprmi  16736  dec2dvds  17110  dec5dvds2  17112  mreexmrid  17701  sinhalfpilem  26523  ppi2i  27230  axlowdimlem13  28987  ex-mod  30481  measvuni  34178  ballotlem2  34453  sgnmulsgp  34515  bnj1224  34777  bnj1541  34832  bnj1311  35000  dfon2lem7  35753  onsucsuccmpi  36409  bj-imn3ani  36553  sbn1ALT  36824  bj-0nelmpt  37082  bj-pinftynminfty  37193  poimirlem30  37610  clsk1indlem4  44006  alimp-no-surprise  48875