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  vnex  5259  opthwiener  5462  epelg  5525  harndom  9467  alephprc  10009  unialeph  10011  ndvdsi  16339  nprmi  16616  dec2dvds  16991  dec5dvds2  16993  mreexmrid  17566  sinhalfpilem  26428  ppi2i  27135  axlowdimlem13  29027  ex-mod  30524  sgnmulsgp  32924  measvuni  34371  ballotlem2  34646  bnj1224  34957  bnj1541  35012  bnj1311  35180  dfon2lem7  35981  onsucsuccmpi  36637  bj-imn3ani  36787  sbn1ALT  37059  bj-0nelmpt  37321  bj-pinftynminfty  37432  poimirlem30  37851  clsk1indlem4  44285  tannpoly  47136  alimp-no-surprise  50026