Theorem mtbi 322

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  mtbir  323  vnexOLD  5253  opthwiener  5468  epelg  5532  harndom  9477  alephprc  10021  unialeph  10023  ndvdsi  16381  nprmi  16658  dec2dvds  17034  dec5dvds2  17036  mreexmrid  17609  sinhalfpilem  26427  ppi2i  27132  axlowdimlem13  29023  ex-mod  30519  sgnmulsgp  32916  measvuni  34358  ballotlem2  34633  bnj1224  34943  bnj1541  34998  bnj1311  35166  dfon2lem7  35969  onsucsuccmpi  36625  bj-imn3ani  36852  sbn1ALT  37165  bj-0nelmpt  37428  bj-pinftynminfty  37541  poimirlem30  37971  clsk1indlem4  44471  tannpoly  47338  alimp-no-surprise  50256