Theorem mtbi 323

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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  mtbir  324  vnexOLD  5247  opthwiener  5462  epelg  5526  harndom  9474  alephprc  10019  unialeph  10021  ndvdsi  16379  nprmi  16656  dec2dvds  17032  dec5dvds2  17034  mreexmrid  17607  sinhalfpilem  26452  ppi2i  27157  axlowdimlem13  29048  ex-mod  30544  sgnmulsgp  32942  measvuni  34405  ballotlem2  34680  bnj1224  34990  bnj1541  35045  bnj1311  35213  dfon2lem7  36022  onsucsuccmpi  36678  bj-imn3ani  36905  sbn1ALT  37218  bj-0nelmpt  37481  bj-pinftynminfty  37594  poimirlem30  38024  clsk1indlem4  44495  tannpoly  47360  alimp-no-surprise  50278