Theorem mtbir 672

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 671	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  851  nndc  852  fal  1371  ax-9  1542  nonconne  2372  nemtbir  2449  ru  2976  noel  3441  iun0  3961  0iun  3962  br0  4069  vprc  4153  iin0r  4190  nlim0  4415  snnex  4469  onsucelsucexmid  4550  0nelxp  4675  dm0  4862  iprc  4916  co02  5163  0fv  5573  frec0g  6426  nnsucuniel  6524  1nen2  6893  fidcenumlemrk  6987  djulclb  7088  ismkvnex  7188  pw1ne3  7264  sucpw1nel3  7267  3nsssucpw1  7270  0nnq  7398  0npr  7517  nqprdisj  7578  0ncn  7865  axpre-ltirr  7916  pnfnre  8034  mnfnre  8035  inelr  8576  xrltnr  9815  fzo0  10204  fzouzdisj  10216  inftonninf  10479  hashinfom  10799  3prm  12171  sqrt2irr  12205  ennnfonelem1  12469  bj-nndcALT  14996  bj-vprc  15134  pwle2  15235  exmidsbthrlem  15258