Theorem mtbir 682

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 681	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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  862  nndc  863  fal  1409  ax-9  1584  nonconne  2432  nemtbir  2509  ru  3050  noel  3525  iun0  4064  0iun  4065  br0  4174  vprc  4260  iin0r  4301  nlim0  4534  snnex  4589  onsucelsucexmid  4672  0nelxp  4797  dm0  4990  iprc  5046  co02  5296  0fv  5728  frec0g  6658  nnsucuniel  6758  1nen2  7152  1ndom2  7156  fidcenumlemrk  7261  djulclb  7385  ismkvnex  7485  pw1ne3  7579  sucpw1nel3  7582  3nsssucpw1  7585  0nnq  7721  0npr  7840  nqprdisj  7901  0ncn  8188  axpre-ltirr  8239  pnfnre  8357  mnfnre  8358  inelr  8902  xrltnr  10160  fzo0  10555  fzouzdisj  10567  inftonninf  10857  hashinfom  11195  lsw0  11330  3prm  12884  sqrt2irr  12918  ballotfilem4  13219  ennnfonelem1  13276  clwwlknnn  16567  konigsberglem4  16646  bj-nndcALT  16700  bj-vprc  16836  pwle2  16942  exmidsbthrlem  16972