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  vnex  5251  opthwiener  5462  epelg  5525  harndom  9470  alephprc  10012  unialeph  10014  ndvdsi  16372  nprmi  16649  dec2dvds  17025  dec5dvds2  17027  mreexmrid  17600  sinhalfpilem  26440  ppi2i  27146  axlowdimlem13  29037  ex-mod  30534  sgnmulsgp  32931  measvuni  34374  ballotlem2  34649  bnj1224  34959  bnj1541  35014  bnj1311  35182  dfon2lem7  35985  onsucsuccmpi  36641  bj-imn3ani  36868  sbn1ALT  37181  bj-0nelmpt  37444  bj-pinftynminfty  37557  poimirlem30  37985  clsk1indlem4  44489  tannpoly  47350  alimp-no-surprise  50268