Theorem mtbi 325

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mtbir  326  vnexOLD  5272  opthwiener  5487  epelg  5552  harndom  9549  alephprc  10171  unialeph  10173  ndvdsi  16575  nprmi  16857  dec2dvds  17234  dec5dvds2  17236  mreexmrid  17810  sinhalfpilem  26785  ppi2i  27489  axlowdimlem13  29525  ex-mod  31043  sgnmulsgp  33416  measvuni  34840  ballotlem2  35114  bnj1224  35424  bnj1541  35479  bnj1311  35647  dfon2lem7  36531  onsucsuccmpi  37211  bj-imn3ani  37437  sbn1ALT  37750  bj-0nelmpt  38017  bj-pinftynminfty  38128  poimirlem30  38548  clsk1indlem4  45029  tannpoly  47909  alimp-no-surprise  50846