Theorem mtbir 312

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

Syntax hints:  ¬ wn 3   ↔ wb 195

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 196

This theorem is referenced by:  fal  1482  nemtbir  2877  ru  3401  pssirr  3669  indifdir  3842  noel  3878  npss0OLD  3967  iun0  4512  0iun  4513  br0  4631  vprc  4724  iin0  4765  nfnid  4823  opelopabsb  4910  0nelxp  5067  0nelxpOLD  5068  dm0  5260  cnv0  5454  co02  5566  nlim0  5700  snsn0non  5763  imadif  5887  0fv  6137  snnex  6862  iprc  6993  tfr2b  7379  tz7.44lem1  7388  tz7.48-3  7426  canth2  7998  pwcdadom  8921  canthp1lem2  9354  pwxpndom2  9366  adderpq  9657  mulerpq  9658  0ncn  9833  ax1ne0  9860  pnfnre  9960  mnfnre  9961  inelr  10887  xrltnr  11829  fzouzdisj  12373  lsw0  13205  fprodn0f  14561  eirr  14772  ruc  14811  aleph1re  14813  sqrt2irr  14817  sadc0  15014  1nprm  15230  3prm  15244  prmrec  15464  meet0  16960  join0  16961  odhash  17812  00lsp  18802  zringndrg  19657  zfbas  21510  ustn0  21834  zclmncvs  22756  lhop  23583  dvrelog  24183  axlowdimlem13  25634  uvtx01vtx  26020  avril1  26711  helloworld  26713  topnfbey  26717  vsfval  26872  dmadjrnb  28149  xrge00  29017  esumrnmpt2  29457  measvuni  29604  sibf0  29723  ballotlem4  29887  signswch  29964  bnj521  30059  3pm3.2ni  30849  elpotr  30930  dfon2lem7  30938  poseq  30994  nosgnn0  31055  sltsolem1  31067  linedegen  31420  mont  31578  subsym1  31596  limsucncmpi  31614  bj-ru1  32125  bj-0nel1  32133  bj-pinftynrr  32286  bj-minftynrr  32290  bj-pinftynminfty  32291  finxp0  32404  poimirlem30  32609  diophren  36395  eqneltri  38272  stoweidlem44  38937  fourierdlem62  39061  salexct2  39233  aisbnaxb  39727  dandysum2p2e4  39814  257prm  40011  fmtno4nprmfac193  40024  139prmALT  40049  31prm  40050  127prm  40053  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  ntrl2v2e  41325  konigsberglem4  41425  0nodd  41600  2nodd  41602  1neven  41722  2zrngnring  41742  ex-gt  42268  alsi-no-surprise  42351