Theorem mtbi 326

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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  mtbir  327  vn0  4238  vnex  5185  opthwiener  5374  epelg  5437  harndom  9060  alephprc  9560  unialeph  9562  ndvdsi  15814  nprmi  16086  dec2dvds  16455  dec5dvds2  16457  mreexmrid  16973  sinhalfpilem  25156  ppi2i  25854  axlowdimlem13  26848  ex-mod  28334  measvuni  31702  ballotlem2  31975  sgnmulsgp  32037  bnj1224  32302  bnj1541  32357  bnj1311  32525  dfon2lem7  33282  onsucsuccmpi  34182  bj-imn3ani  34316  bj-0nelmpt  34812  bj-pinftynminfty  34923  poimirlem30  35368  clsk1indlem4  41121  alimp-no-surprise  45701