Theorem mtbir 326

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3pm3.2ni  1519  fal  1584  eqneltri  2881  nemtbir  3053  ru  3741  pssirrOLD  4055  noel  4287  vn0  4294  vn0OLD  4295  uni0  4899  iun0  5024  0iun  5025  br0  5158  vprcOLD  5282  iin0  5331  nfnid  5344  opelopabsb  5512  0nelopab  5548  0nelxp  5693  nrelvOLD  5785  cnv0  5867  cnv0OLD  5868  dm0  5908  co02  6261  nlim0  6422  snsn0non  6488  imadif  6621  0fv  6923  poxp2  8145  poseq  8160  tz7.44lem1  8398  nlim1  8480  nlim2  8481  sdom0  9111  canth2  9132  snnen2o  9219  1sdom2  9222  canthp1lem2  10666  pwxpndom2  10678  adderpq  10969  mulerpq  10970  0ncn  11146  ax1ne0  11173  inelr  12236  xrltnr  13174  fzouzdisj  13755  lsw0  14634  eirr  16299  ruc  16337  aleph1re  16339  sqrt2irr  16343  n2dvds1  16464  n2dvds3  16467  sadc0  16550  1nprm  16775  join0  18497  meet0  18498  smndex1n0mnd  19030  nsmndex1  19031  smndex2dnrinv  19033  degenmgmnfn  19055  degenmgm2nfun  19058  odhash  19707  cnfldfun  21605  zringndrg  21687  zfbas  24128  ustn0  24453  zclmncvs  25382  lhop  26250  dvrelog  26882  nosgnn0  27902  ltssolem1  27919  addsrid  28237  muls01  28385  mulsrid  28386  axlowdimlem13  29419  ntrl2v2e  30646  konigsberglem4  30743  avril1  30951  helloworld  30953  topnfbey  30957  nowisdomv  30962  vsfval  31122  dmadjrnb  32395  xrge00  33462  domnprodeq0  33727  esumrnmpt2  34586  measvuni  34733  sibf0  34853  ballotlem4  35018  signswch  35077  satf0n0  35965  fmlaomn0  35977  gonan0  35979  goaln0  35980  fmla0disjsuc  35985  elpotr  36366  dfon2lem7  36374  linedegen  36731  nmotru  37035  limsucncmpi  37072  mh-inf3sn  37169  bj-ru1  37695  bj-0nel1  37705  bj-inftyexpitaudisj  37965  bj-pinftynminfty  37987  finxp0  38153  poimirlem30  38407  coss0  39325  epnsymrel  39402  sn-inelr  43383  diophren  43662  permaxnul  45839  permaxinf2lem  45843  notbicom  46005  rexanuz2nf  46328  stoweidlem44  46880  fourierdlem62  47004  salexct2  47175  chnerlem1  47718  aisbnaxb  47807  dandysum2p2e4  47894  iota0ndef  47935  aiota0ndef  47993  257prm  48472  fmtno4nprmfac193  48485  139prmALT  48507  31prm  48508  127prm  48510  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  usgrexmpl2trifr  48961  0nodd  49093  2nodd  49095  1neven  49161  2zrngnring  49181  ex-gt  50662  als-no-surprise  50743  rals-no-surprise  50744