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  5283  opthwiener  5499  epelg  5564  harndom  9527  alephprc  10095  unialeph  10097  ndvdsi  16487  nprmi  16764  dec2dvds  17140  dec5dvds2  17142  mreexmrid  17716  sinhalfpilem  26657  ppi2i  27362  axlowdimlem13  29333  ex-mod  30829  sgnmulsgp  33205  measvuni  34628  ballotlem2  34903  bnj1224  35213  bnj1541  35268  bnj1311  35436  dfon2lem7  36292  onsucsuccmpi  36987  bj-imn3ani  37213  sbn1ALT  37526  bj-0nelmpt  37791  bj-pinftynminfty  37904  poimirlem30  38334  clsk1indlem4  44803  tannpoly  47660  alimp-no-surprise  50592