Theorem mtbir 678

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 677	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  858  nndc  859  fal  1405  ax-9  1580  nonconne  2415  nemtbir  2492  ru  3031  noel  3500  iun0  4032  0iun  4033  br0  4142  vprc  4226  iin0r  4265  nlim0  4497  snnex  4551  onsucelsucexmid  4634  0nelxp  4759  dm0  4951  iprc  5007  co02  5257  0fv  5686  frec0g  6606  nnsucuniel  6706  1nen2  7090  1ndom2  7094  fidcenumlemrk  7196  djulclb  7297  ismkvnex  7397  pw1ne3  7491  sucpw1nel3  7494  3nsssucpw1  7497  0nnq  7627  0npr  7746  nqprdisj  7807  0ncn  8094  axpre-ltirr  8145  pnfnre  8263  mnfnre  8264  inelr  8806  xrltnr  10058  fzo0  10450  fzouzdisj  10462  inftonninf  10750  hashinfom  11086  lsw0  11210  3prm  12763  sqrt2irr  12797  ennnfonelem1  13091  clwwlknnn  16336  konigsberglem4  16415  bj-nndcALT  16459  bj-vprc  16595  pwle2  16703  exmidsbthrlem  16733