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  5271  opthwiener  5486  epelg  5551  harndom  9560  alephprc  10182  unialeph  10184  ndvdsi  16588  nprmi  16870  dec2dvds  17247  dec5dvds2  17249  mreexmrid  17823  sinhalfpilem  26798  ppi2i  27502  axlowdimlem13  29538  ex-mod  31056  sgnmulsgp  33470  measvuni  34894  ballotlem2  35168  bnj1224  35478  bnj1541  35533  bnj1311  35701  dfon2lem7  36644  onsucsuccmpi  37324  bj-imn3ani  37550  sbn1ALT  37863  bj-0nelmpt  38131  bj-pinftynminfty  38242  poimirlem30  38662  clsk1indlem4  45138  tannpoly  48034  alimp-no-surprise  51046