Theorem mtbir 660

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

Syntax hints:  ¬ wn 3   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnexmid  835  nndc  836  fal  1338  ax-9  1511  nonconne  2318  nemtbir  2395  ru  2903  noel  3362  iun0  3864  0iun  3865  br0  3971  vprc  4055  iin0r  4088  nlim0  4311  snnex  4364  onsucelsucexmid  4440  0nelxp  4562  dm0  4748  iprc  4802  co02  5047  0fv  5449  frec0g  6287  nnsucuniel  6384  1nen2  6748  fidcenumlemrk  6835  djulclb  6933  ismkvnex  7022  0nnq  7165  0npr  7284  nqprdisj  7345  0ncn  7632  axpre-ltirr  7683  pnfnre  7800  mnfnre  7801  inelr  8339  xrltnr  9559  fzo0  9938  fzouzdisj  9950  inftonninf  10207  hashinfom  10517  3prm  11798  sqrt2irr  11829  ennnfonelem1  11909  bj-nndcALT  12952  bj-vprc  13083  pwle2  13182  exmidsbthrlem  13206