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  1545  nonconne  2379  nemtbir  2456  ru  2988  noel  3455  iun0  3974  0iun  3975  br0  4082  vprc  4166  iin0r  4203  nlim0  4430  snnex  4484  onsucelsucexmid  4567  0nelxp  4692  dm0  4881  iprc  4935  co02  5184  0fv  5597  frec0g  6464  nnsucuniel  6562  1nen2  6931  fidcenumlemrk  7029  djulclb  7130  ismkvnex  7230  pw1ne3  7315  sucpw1nel3  7318  3nsssucpw1  7321  0nnq  7450  0npr  7569  nqprdisj  7630  0ncn  7917  axpre-ltirr  7968  pnfnre  8087  mnfnre  8088  inelr  8630  xrltnr  9873  fzo0  10263  fzouzdisj  10275  inftonninf  10553  hashinfom  10889  3prm  12323  sqrt2irr  12357  ennnfonelem1  12651  bj-nndcALT  15512  bj-vprc  15650  pwle2  15753  exmidsbthrlem  15779