Theorem mtbi 321

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  mtbir  322  vn0  4341  vnex  5319  opthwiener  5520  epelg  5587  harndom  9605  alephprc  10142  unialeph  10144  ndvdsi  16414  nprmi  16690  dec2dvds  17065  dec5dvds2  17067  mreexmrid  17656  sinhalfpilem  26491  ppi2i  27197  axlowdimlem13  28888  ex-mod  30382  measvuni  34047  ballotlem2  34322  sgnmulsgp  34384  bnj1224  34646  bnj1541  34701  bnj1311  34869  dfon2lem7  35613  onsucsuccmpi  36155  bj-imn3ani  36292  sbn1ALT  36563  bj-0nelmpt  36823  bj-pinftynminfty  36934  poimirlem30  37351  clsk1indlem4  43711  alimp-no-surprise  48529