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  4298  vnex  5256  opthwiener  5461  epelg  5524  harndom  9473  alephprc  10012  unialeph  10014  ndvdsi  16341  nprmi  16618  dec2dvds  16993  dec5dvds2  16995  mreexmrid  17567  sinhalfpilem  26388  ppi2i  27095  axlowdimlem13  28917  ex-mod  30411  sgnmulsgp  32801  measvuni  34183  ballotlem2  34459  bnj1224  34770  bnj1541  34825  bnj1311  34993  dfon2lem7  35765  onsucsuccmpi  36419  bj-imn3ani  36563  sbn1ALT  36834  bj-0nelmpt  37092  bj-pinftynminfty  37203  poimirlem30  37632  clsk1indlem4  44020  tannpoly  46878  alimp-no-surprise  49770