Theorem mtbir 323

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  3pm3.2ni  1490  fal  1555  eqneltri  2852  nemtbir  3025  ru  3735  ruOLD  3736  pssirr  4052  noel  4287  vn0  4294  uni0  4888  iun0  5014  0iun  5015  br0  5144  vprc  5257  iin0  5304  nfnid  5317  opelopabsb  5475  0nelopab  5510  0nelxp  5655  nrelv  5746  dm0  5866  cnv0  6093  cnv0OLD  6094  co02  6215  nlim0  6373  snsn0non  6439  imadif  6572  0fv  6871  poxp2  8081  poseq  8096  tz7.44lem1  8332  nlim1  8412  nlim2  8413  sdom0  9031  canth2  9052  snnen2o  9138  1sdom2  9141  canthp1lem2  10553  pwxpndom2  10565  adderpq  10856  mulerpq  10857  0ncn  11033  ax1ne0  11060  inelr  12124  xrltnr  13022  fzouzdisj  13599  lsw0  14476  eirr  16118  ruc  16156  aleph1re  16158  sqrt2irr  16162  n2dvds1  16283  n2dvds3  16286  sadc0  16369  1nprm  16594  join0  18313  meet0  18314  smndex1n0mnd  18824  nsmndex1  18825  smndex2dnrinv  18827  odhash  19490  cnfldfun  21309  cnfldfunOLD  21322  zringndrg  21409  zfbas  23814  ustn0  24139  zclmncvs  25078  lhop  25951  dvrelog  26576  nosgnn0  27600  sltsolem1  27617  addsrid  27910  muls01  28054  mulsrid  28055  axlowdimlem13  28936  ntrl2v2e  30142  konigsberglem4  30239  avril1  30447  helloworld  30449  topnfbey  30453  vsfval  30617  dmadjrnb  31890  xrge00  33004  esumrnmpt2  34104  measvuni  34250  sibf0  34370  ballotlem4  34535  signswch  34597  satf0n0  35445  fmlaomn0  35457  gonan0  35459  goaln0  35460  fmla0disjsuc  35465  elpotr  35846  dfon2lem7  35854  linedegen  36210  nmotru  36475  limsucncmpi  36512  bj-ru1  37010  bj-0nel1  37020  bj-inftyexpitaudisj  37272  bj-pinftynminfty  37294  finxp0  37458  poimirlem30  37713  coss0  38604  epnsymrel  38681  sn-inelr  42608  diophren  42933  permaxnul  45128  permaxinf2lem  45132  notbicom  45289  rexanuz2nf  45617  stoweidlem44  46169  fourierdlem62  46293  salexct2  46464  chnerlem1  47007  aisbnaxb  47038  dandysum2p2e4  47125  iota0ndef  47166  aiota0ndef  47224  257prm  47688  fmtno4nprmfac193  47701  139prmALT  47723  31prm  47724  127prm  47726  nnsum4primeseven  47927  nnsum4primesevenALTV  47928  usgrexmpl2trifr  48164  0nodd  48297  2nodd  48299  1neven  48365  2zrngnring  48385  ex-gt  49856  alsi-no-surprise  49924