Theorem mtbir 313

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

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  fal  1488  nemtbir  2886  ru  3428  pssirr  3699  indifdir  3875  noel  3911  npss0OLD  4006  iun0  4567  0iun  4568  br0  4692  vprc  4787  iin0  4830  nfnid  4888  opelopabsb  4975  0nelxp  5133  0nelxpOLD  5134  0xp  5189  dm0  5328  cnv0  5523  co02  5637  nlim0  5771  snsn0non  5834  imadif  5961  0fv  6214  snnexOLD  6952  iprc  7086  tfr2b  7477  tz7.44lem1  7486  tz7.48-3  7524  canth2  8098  pwcdadom  9023  canthp1lem2  9460  pwxpndom2  9472  adderpq  9763  mulerpq  9764  0ncn  9939  ax1ne0  9966  pnfnre  10066  mnfnre  10067  inelr  10995  xrltnr  11938  fzouzdisj  12488  lsw0  13335  fprodn0f  14703  eirr  14914  ruc  14953  aleph1re  14955  sqrt2irr  14960  sadc0  15157  1nprm  15373  3prm  15387  prmrec  15607  meet0  17118  join0  17119  odhash  17970  00lsp  18962  cnfldfunALT  19740  zringndrg  19819  zfbas  21681  ustn0  22005  zclmncvs  22929  lhop  23760  dvrelog  24364  axlowdimlem13  25815  ntrl2v2e  26998  konigsberglem4  27097  avril1  27289  helloworld  27291  topnfbey  27295  vsfval  27458  dmadjrnb  28735  xrge00  29660  esumrnmpt2  30104  measvuni  30251  sibf0  30370  ballotlem4  30534  signswch  30612  bnj521  30779  3pm3.2ni  31569  elpotr  31660  dfon2lem7  31668  poseq  31724  nosgnn0  31785  sltsolem1  31800  linedegen  32225  mont  32383  subsym1  32401  limsucncmpi  32419  bj-ru1  32908  bj-0nel1  32915  bj-pinftynrr  33080  bj-minftynrr  33084  bj-pinftynminfty  33085  finxp0  33199  poimirlem30  33410  diophren  37196  eqneltri  39066  stoweidlem44  40024  fourierdlem62  40148  salexct2  40320  aisbnaxb  40841  dandysum2p2e4  40928  257prm  41238  fmtno4nprmfac193  41251  139prmALT  41276  31prm  41277  127prm  41280  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  0nodd  41575  2nodd  41577  1neven  41697  2zrngnring  41717  ex-gt  42234  alsi-no-surprise  42307