Theorem mtbir 677

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 676	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  857  nndc  858  fal  1404  ax-9  1579  nonconne  2414  nemtbir  2491  ru  3030  noel  3498  iun0  4027  0iun  4028  br0  4137  vprc  4221  iin0r  4259  nlim0  4491  snnex  4545  onsucelsucexmid  4628  0nelxp  4753  dm0  4945  iprc  5001  co02  5250  0fv  5677  frec0g  6562  nnsucuniel  6662  1nen2  7046  1ndom2  7050  fidcenumlemrk  7152  djulclb  7253  ismkvnex  7353  pw1ne3  7447  sucpw1nel3  7450  3nsssucpw1  7453  0nnq  7583  0npr  7702  nqprdisj  7763  0ncn  8050  axpre-ltirr  8101  pnfnre  8220  mnfnre  8221  inelr  8763  xrltnr  10013  fzo0  10404  fzouzdisj  10416  inftonninf  10703  hashinfom  11039  lsw0  11160  3prm  12699  sqrt2irr  12733  ennnfonelem1  13027  clwwlknnn  16262  bj-nndcALT  16354  bj-vprc  16491  pwle2  16599  exmidsbthrlem  16626