Theorem mtbir 661

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 660	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 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnexmid  840  nndc  841  fal  1349  ax-9  1518  nonconne  2346  nemtbir  2423  ru  2945  noel  3408  iun0  3916  0iun  3917  br0  4024  vprc  4108  iin0r  4142  nlim0  4366  snnex  4420  onsucelsucexmid  4501  0nelxp  4626  dm0  4812  iprc  4866  co02  5111  0fv  5515  frec0g  6356  nnsucuniel  6454  1nen2  6818  fidcenumlemrk  6910  djulclb  7011  ismkvnex  7110  pw1ne3  7177  sucpw1nel3  7180  3nsssucpw1  7183  0nnq  7296  0npr  7415  nqprdisj  7476  0ncn  7763  axpre-ltirr  7814  pnfnre  7931  mnfnre  7932  inelr  8473  xrltnr  9706  fzo0  10093  fzouzdisj  10105  inftonninf  10366  hashinfom  10680  3prm  12039  sqrt2irr  12071  ennnfonelem1  12277  bj-nndcALT  13472  bj-vprc  13613  pwle2  13712  exmidsbthrlem  13735