Theorem mtbi 324

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  mtbir  325  vnex  5221  opthwiener  5407  epelg  5469  harndom  9031  alephprc  9528  unialeph  9530  ndvdsi  15766  nprmi  16036  dec2dvds  16402  dec5dvds2  16404  mreexmrid  16917  sinhalfpilem  25052  ppi2i  25749  axlowdimlem13  26743  ex-mod  28231  measvuni  31477  ballotlem2  31750  sgnmulsgp  31812  bnj1224  32077  bnj1541  32132  bnj1311  32300  dfon2lem7  33038  onsucsuccmpi  33795  bj-imn3ani  33925  bj-0nelmpt  34412  bj-pinftynminfty  34513  poimirlem30  34926  clsk1indlem4  40400  alimp-no-surprise  44889