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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  mtbir  323  vn0  4339  vnex  5315  opthwiener  5515  epelg  5582  harndom  9557  alephprc  10094  unialeph  10096  ndvdsi  16355  nprmi  16626  dec2dvds  16996  dec5dvds2  16998  mreexmrid  17587  sinhalfpilem  25973  ppi2i  26673  axlowdimlem13  28212  ex-mod  29702  measvuni  33212  ballotlem2  33487  sgnmulsgp  33549  bnj1224  33812  bnj1541  33867  bnj1311  34035  dfon2lem7  34761  onsucsuccmpi  35328  bj-imn3ani  35465  sbn1ALT  35737  bj-0nelmpt  35997  bj-pinftynminfty  36108  poimirlem30  36518  clsk1indlem4  42795  alimp-no-surprise  47828