Theorem mtbir 677

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 132	. 2 ⊢ (𝜓 ↔ 𝜑)
4	1, 3	mtbi 676	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  857  nndc  858  fal  1404  ax-9  1579  nonconne  2414  nemtbir  2491  ru  3030  noel  3498  iun0  4027  0iun  4028  br0  4137  vprc  4221  iin0r  4259  nlim0  4491  snnex  4545  onsucelsucexmid  4628  0nelxp  4753  dm0  4945  iprc  5001  co02  5250  0fv  5677  frec0g  6563  nnsucuniel  6663  1nen2  7047  1ndom2  7051  fidcenumlemrk  7153  djulclb  7254  ismkvnex  7354  pw1ne3  7448  sucpw1nel3  7451  3nsssucpw1  7454  0nnq  7584  0npr  7703  nqprdisj  7764  0ncn  8051  axpre-ltirr  8102  pnfnre  8221  mnfnre  8222  inelr  8764  xrltnr  10014  fzo0  10405  fzouzdisj  10417  inftonninf  10705  hashinfom  11041  lsw0  11165  3prm  12718  sqrt2irr  12752  ennnfonelem1  13046  clwwlknnn  16282  konigsberglem4  16361  bj-nndcALT  16405  bj-vprc  16542  pwle2  16650  exmidsbthrlem  16677