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 ⊢ ¬ 𝜓

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mtbir  326  vnexOLD  5275  opthwiener  5491  epelg  5556  harndom  9534  alephprc  10102  unialeph  10104  ndvdsi  16502  nprmi  16779  dec2dvds  17155  dec5dvds2  17157  mreexmrid  17731  sinhalfpilem  26701  ppi2i  27405  axlowdimlem13  29411  ex-mod  30929  sgnmulsgp  33302  measvuni  34725  ballotlem2  35000  bnj1224  35310  bnj1541  35365  bnj1311  35533  dfon2lem7  36366  onsucsuccmpi  37062  bj-imn3ani  37288  sbn1ALT  37601  bj-0nelmpt  37866  bj-pinftynminfty  37979  poimirlem30  38399  clsk1indlem4  44884  tannpoly  47758  alimp-no-surprise  50710