Theorem mtbi 325

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  326  vnexOLD  5283  opthwiener  5498  epelg  5563  harndom  9524  alephprc  10083  unialeph  10085  ndvdsi  16470  nprmi  16747  dec2dvds  17123  dec5dvds2  17125  mreexmrid  17699  sinhalfpilem  26594  ppi2i  27299  axlowdimlem13  29245  ex-mod  30741  sgnmulsgp  33117  measvuni  34549  ballotlem2  34824  bnj1224  35134  bnj1541  35189  bnj1311  35357  dfon2lem7  36178  onsucsuccmpi  36843  bj-imn3ani  37069  sbn1ALT  37382  bj-0nelmpt  37646  bj-pinftynminfty  37759  poimirlem30  38189  clsk1indlem4  44662  tannpoly  47516  alimp-no-surprise  50444