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  4308  vnex  5269  opthwiener  5474  epelg  5539  harndom  9515  alephprc  10052  unialeph  10054  ndvdsi  16382  nprmi  16659  dec2dvds  17034  dec5dvds2  17036  mreexmrid  17604  sinhalfpilem  26372  ppi2i  27079  axlowdimlem13  28881  ex-mod  30378  sgnmulsgp  32768  measvuni  34204  ballotlem2  34480  bnj1224  34791  bnj1541  34846  bnj1311  35014  dfon2lem7  35777  onsucsuccmpi  36431  bj-imn3ani  36575  sbn1ALT  36846  bj-0nelmpt  37104  bj-pinftynminfty  37215  poimirlem30  37644  clsk1indlem4  44033  alimp-no-surprise  49767