Theorem mtbir 315

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

Syntax hints:  ¬ wn 3   ↔ wb 198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  fal  1521  eqneltri  2860  nemtbir  3064  ru  3681  pssirr  3968  indifdir  4148  noel  4184  noelOLD  4185  iun0  4851  0iun  4852  br0  4978  vprc  5076  iin0  5115  nfnid  5129  opelopabsb  5271  0nelxp  5441  0xp  5499  nrelv  5523  dm0  5637  cnv0  5839  co02  5952  nlim0  6087  snsn0non  6147  imadif  6271  0fv  6539  tz7.44lem1  7845  canth2  8466  canthp1lem2  9873  pwxpndom2  9885  adderpq  10176  mulerpq  10177  0ncn  10353  ax1ne0  10380  inelr  11429  xrltnr  12331  fzouzdisj  12888  lsw0  13728  eirr  15418  ruc  15456  aleph1re  15458  sqrt2irr  15462  n2dvds1  15577  n2dvds3  15581  sadc0  15663  1nprm  15879  meet0  17605  join0  17606  odhash  18460  cnfldfunALT  20260  zringndrg  20339  zfbas  22208  ustn0  22532  zclmncvs  23455  lhop  24316  dvrelog  24921  axlowdimlem13  26443  ntrl2v2e  27687  konigsberglem4  27787  avril1  28019  helloworld  28021  topnfbey  28025  vsfval  28187  dmadjrnb  29464  xrge00  30402  esumrnmpt2  30968  measvuni  31115  sibf0  31234  ballotlem4  31399  signswch  31474  bnj521  31652  satf0n0  32185  3pm3.2ni  32460  elpotr  32543  dfon2lem7  32551  poseq  32613  nosgnn0  32683  sltsolem1  32698  linedegen  33122  nmotru  33274  subsym1  33292  limsucncmpi  33310  bj-ru1  33746  bj-0nel1  33758  bj-inftyexpitaudisj  33953  bj-pinftynminfty  33975  finxp0  34110  poimirlem30  34360  coss0  35161  epnsymrel  35240  diophren  38803  stoweidlem44  41758  fourierdlem62  41882  salexct2  42051  aisbnaxb  42575  dandysum2p2e4  42662  iota0ndef  42677  aiota0ndef  42699  257prm  43089  fmtno4nprmfac193  43102  139prmALT  43125  31prm  43126  127prm  43129  nnsum4primeseven  43331  nnsum4primesevenALTV  43332  0nodd  43443  2nodd  43445  1neven  43565  2zrngnring  43585  ex-gt  44192  alsi-no-surprise  44262