Theorem mtbir 675

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 674	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  855  nndc  856  fal  1402  ax-9  1577  nonconne  2412  nemtbir  2489  ru  3028  noel  3496  iun0  4025  0iun  4026  br0  4135  vprc  4219  iin0r  4257  nlim0  4489  snnex  4543  onsucelsucexmid  4626  0nelxp  4751  dm0  4943  iprc  4999  co02  5248  0fv  5673  frec0g  6558  nnsucuniel  6658  1nen2  7042  1ndom2  7046  fidcenumlemrk  7144  djulclb  7245  ismkvnex  7345  pw1ne3  7438  sucpw1nel3  7441  3nsssucpw1  7444  0nnq  7574  0npr  7693  nqprdisj  7754  0ncn  8041  axpre-ltirr  8092  pnfnre  8211  mnfnre  8212  inelr  8754  xrltnr  10004  fzo0  10395  fzouzdisj  10407  inftonninf  10694  hashinfom  11030  lsw0  11151  3prm  12690  sqrt2irr  12724  ennnfonelem1  13018  clwwlknnn  16207  bj-nndcALT  16290  bj-vprc  16427  pwle2  16535  exmidsbthrlem  16562