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 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  3pm3.2ni  1519  fal  1584  eqneltri  2882  nemtbir  3054  ru  3744  pssirrOLD  4059  noel  4292  vn0  4299  vn0OLD  4300  uni0  4902  iun0  5027  0iun  5028  br0  5161  vprcOLD  5285  iin0  5335  nfnid  5348  opelopabsb  5516  0nelopab  5552  0nelxp  5697  nrelvOLD  5789  cnv0  5871  cnv0OLD  5872  dm0  5912  co02  6264  nlim0  6423  snsn0non  6489  imadif  6622  0fv  6924  poxp2  8140  poseq  8155  tz7.44lem1  8393  nlim1  8475  nlim2  8476  sdom0  9098  canth2  9119  snnen2o  9206  1sdom2  9209  canthp1lem2  10639  pwxpndom2  10651  adderpq  10942  mulerpq  10943  0ncn  11119  ax1ne0  11146  inelr  12209  xrltnr  13145  fzouzdisj  13726  lsw0  14604  eirr  16262  ruc  16300  aleph1re  16302  sqrt2irr  16306  n2dvds1  16427  n2dvds3  16430  sadc0  16513  1nprm  16738  join0  18460  meet0  18461  smndex1n0mnd  18975  nsmndex1  18976  smndex2dnrinv  18978  odhash  19645  cnfldfun  21517  zringndrg  21599  zfbas  24034  ustn0  24359  zclmncvs  25288  lhop  26156  dvrelog  26783  nosgnn0  27803  ltssolem1  27820  addsrid  28138  muls01  28286  mulsrid  28287  axlowdimlem13  29285  ntrl2v2e  30490  konigsberglem4  30587  avril1  30795  helloworld  30797  topnfbey  30801  nowisdomv  30806  vsfval  30966  dmadjrnb  32239  xrge00  33315  domnprodeq0  33580  esumrnmpt2  34439  measvuni  34585  sibf0  34705  ballotlem4  34870  signswch  34929  satf0n0  35851  fmlaomn0  35863  gonan0  35865  goaln0  35866  fmla0disjsuc  35871  elpotr  36252  dfon2lem7  36260  linedegen  36616  nmotru  36900  limsucncmpi  36937  mh-inf3sn  37034  bj-ru1  37560  bj-0nel1  37570  bj-inftyexpitaudisj  37830  bj-pinftynminfty  37852  finxp0  38018  poimirlem30  38282  coss0  39199  epnsymrel  39276  sn-inelr  43242  diophren  43523  permaxnul  45700  permaxinf2lem  45704  notbicom  45866  rexanuz2nf  46189  stoweidlem44  46741  fourierdlem62  46865  salexct2  47036  chnerlem1  47581  aisbnaxb  47631  dandysum2p2e4  47718  iota0ndef  47759  aiota0ndef  47817  257prm  48296  fmtno4nprmfac193  48309  139prmALT  48331  31prm  48332  127prm  48334  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  usgrexmpl2trifr  48785  0nodd  48918  2nodd  48920  1neven  48986  2zrngnring  49006  ex-gt  50489  als-no-surprise  50567  rals-no-surprise  50568