Theorem mtbir 596

Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)

Hypotheses

Ref	Expression
mtbir.1	⊢ ¬ 𝜓
mtbir.2	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mtbir	⊢ ¬ 𝜑

Proof of Theorem mtbir

Step	Hyp	Ref	Expression
1		mtbir.1	. 2 ⊢ ¬ 𝜓
2		mtbir.2	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	bicomi 123	. 2 ⊢ (𝜓 ↔ 𝜑)
4	1, 3	mtbi 595	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  fal  1250  ax-9  1424  nonconne  2217  nemtbir  2294  ru  2763  pssirr  3044  noel  3228  npss0  3266  iun0  3713  0iun  3714  vprc  3888  iin0r  3922  nlim0  4131  snnex  4181  onsucelsucexmid  4255  0nelxp  4372  dm0  4549  iprc  4600  co02  4834  0fv  5208  frec0g  5983  0nnq  6462  0npr  6581  nqprdisj  6642  0ncn  6908  axpre-ltirr  6956  pnfnre  7067  mnfnre  7068  inelr  7575  xrltnr  8701  fzo0  9024  fzouzdisj  9036  sqrt2irr  9878  nnexmid  9899  nndc  9900  bj-vprc  10016