Theorem mtbir 666

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

Syntax hints:  ¬ wn 3   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnexmid  845  nndc  846  fal  1355  ax-9  1524  nonconne  2352  nemtbir  2429  ru  2954  noel  3418  iun0  3929  0iun  3930  br0  4037  vprc  4121  iin0r  4155  nlim0  4379  snnex  4433  onsucelsucexmid  4514  0nelxp  4639  dm0  4825  iprc  4879  co02  5124  0fv  5531  frec0g  6376  nnsucuniel  6474  1nen2  6839  fidcenumlemrk  6931  djulclb  7032  ismkvnex  7131  pw1ne3  7207  sucpw1nel3  7210  3nsssucpw1  7213  0nnq  7326  0npr  7445  nqprdisj  7506  0ncn  7793  axpre-ltirr  7844  pnfnre  7961  mnfnre  7962  inelr  8503  xrltnr  9736  fzo0  10124  fzouzdisj  10136  inftonninf  10397  hashinfom  10712  3prm  12082  sqrt2irr  12116  ennnfonelem1  12362  bj-nndcALT  13793  bj-vprc  13931  pwle2  14031  exmidsbthrlem  14054