Theorem mtbir 673

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 672	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  852  nndc  853  fal  1380  ax-9  1555  nonconne  2389  nemtbir  2466  ru  3001  noel  3468  iun0  3989  0iun  3990  br0  4099  vprc  4183  iin0r  4220  nlim0  4448  snnex  4502  onsucelsucexmid  4585  0nelxp  4710  dm0  4900  iprc  4955  co02  5204  0fv  5624  frec0g  6495  nnsucuniel  6593  1nen2  6972  fidcenumlemrk  7070  djulclb  7171  ismkvnex  7271  pw1ne3  7357  sucpw1nel3  7360  3nsssucpw1  7363  0nnq  7492  0npr  7611  nqprdisj  7672  0ncn  7959  axpre-ltirr  8010  pnfnre  8129  mnfnre  8130  inelr  8672  xrltnr  9916  fzo0  10307  fzouzdisj  10319  inftonninf  10604  hashinfom  10940  lsw0  11058  3prm  12520  sqrt2irr  12554  ennnfonelem1  12848  bj-nndcALT  15828  bj-vprc  15966  pwle2  16070  exmidsbthrlem  16096