Theorem mtbir 629

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

Syntax hints:  ¬ wn 3   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  fal  1294  ax-9  1467  nonconne  2263  nemtbir  2340  ru  2828  noel  3279  iun0  3771  0iun  3772  vprc  3948  iin0r  3981  nlim0  4197  snnex  4247  onsucelsucexmid  4321  0nelxp  4440  dm0  4620  iprc  4671  co02  4912  0fv  5304  frec0g  6118  nnsucuniel  6212  1nen2  6531  djulclb  6694  0nnq  6870  0npr  6989  nqprdisj  7050  0ncn  7316  axpre-ltirr  7364  pnfnre  7476  mnfnre  7477  inelr  8005  xrltnr  9185  fzo0  9510  fzouzdisj  9522  inftonninf  9778  hashinfom  10086  3prm  11016  sqrt2irr  11047  nnexmid  11129  nndc  11130  bj-vprc  11256  exmidsbthrlem  11381