Theorem mtbir 629

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

Syntax hints:  ¬ wn 3   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  fal  1292  ax-9  1465  nonconne  2261  nemtbir  2338  ru  2825  noel  3273  iun0  3760  0iun  3761  vprc  3936  iin0r  3969  nlim0  4185  snnex  4235  onsucelsucexmid  4309  0nelxp  4428  dm0  4608  iprc  4659  co02  4898  0fv  5284  frec0g  6094  nnsucuniel  6188  1nen2  6507  djulclb  6654  0nnq  6826  0npr  6945  nqprdisj  7006  0ncn  7272  axpre-ltirr  7320  pnfnre  7432  mnfnre  7433  inelr  7961  xrltnr  9145  fzo0  9468  fzouzdisj  9480  inftonninf  9736  hashinfom  10021  3prm  10890  sqrt2irr  10921  nnexmid  11003  nndc  11004  bj-vprc  11130  exmidsbthrlem  11254