Theorem mtbi 313

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

Syntax hints:  ¬ wn 3   ↔ wb 197

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 198

This theorem is referenced by:  mtbir  314  vnex  4959  opthwiener  5137  harndom  8680  alephprc  9177  unialeph  9179  ndvdsi  15431  bitsfzo  15452  nprmi  15696  dec2dvds  16060  dec5dvds2  16062  mreexmrid  16583  sinhalfpilem  24521  ppi2i  25200  axlowdimlem13  26139  ex-mod  27786  measvuni  30745  ballotlem2  31019  sgnmulsgp  31081  bnj1224  31341  bnj1541  31395  bnj1311  31561  dfon2lem7  32158  onsucsuccmpi  32902  bj-imn3ani  33029  bj-0nelmpt  33518  bj-pinftynminfty  33569  poimirlem30  33884  clsk1indlem4  39040  alimp-no-surprise  43223