Theorem mtbir 634

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 633	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  fal  1303  ax-9  1476  nonconne  2274  nemtbir  2351  ru  2853  noel  3306  iun0  3808  0iun  3809  vprc  3992  iin0r  4025  nlim0  4245  snnex  4298  onsucelsucexmid  4374  0nelxp  4495  dm0  4681  iprc  4733  co02  4978  0fv  5374  frec0g  6200  nnsucuniel  6296  1nen2  6657  fidcenumlemrk  6743  djulclb  6827  0nnq  7020  0npr  7139  nqprdisj  7200  0ncn  7466  axpre-ltirr  7514  pnfnre  7626  mnfnre  7627  inelr  8158  xrltnr  9349  fzo0  9728  fzouzdisj  9740  inftonninf  9996  hashinfom  10317  3prm  11552  sqrt2irr  11583  nnexmid  12372  nndc  12373  bj-vprc  12499  exmidsbthrlem  12621