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  vn0  4295  vnex  5252  opthwiener  5454  epelg  5517  harndom  9448  alephprc  9990  unialeph  9992  ndvdsi  16323  nprmi  16600  dec2dvds  16975  dec5dvds2  16977  mreexmrid  17549  sinhalfpilem  26400  ppi2i  27107  axlowdimlem13  28933  ex-mod  30427  sgnmulsgp  32824  measvuni  34225  ballotlem2  34500  bnj1224  34811  bnj1541  34866  bnj1311  35034  dfon2lem7  35829  onsucsuccmpi  36483  bj-imn3ani  36627  sbn1ALT  36898  bj-0nelmpt  37156  bj-pinftynminfty  37267  poimirlem30  37696  clsk1indlem4  44083  tannpoly  46927  alimp-no-surprise  49819