Theorem mtbi 324

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  mtbir  325  vnexOLD  5265  opthwiener  5480  epelg  5544  harndom  9503  alephprc  10048  unialeph  10050  ndvdsi  16436  nprmi  16713  dec2dvds  17089  dec5dvds2  17091  mreexmrid  17665  sinhalfpilem  26515  ppi2i  27220  axlowdimlem13  29111  ex-mod  30607  sgnmulsgp  32994  measvuni  34471  ballotlem2  34746  bnj1224  35056  bnj1541  35111  bnj1311  35279  dfon2lem7  36097  onsucsuccmpi  36763  bj-imn3ani  36990  sbn1ALT  37303  bj-0nelmpt  37566  bj-pinftynminfty  37679  poimirlem30  38109  clsk1indlem4  44580  tannpoly  47444  alimp-no-surprise  50362