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  1554  eqneltri  2860  nemtbir  3038  ru  3786  ruOLD  3787  pssirr  4103  noel  4338  iun0  5062  0iun  5063  br0  5192  vprc  5315  iin0  5362  nfnid  5375  opelopabsb  5535  0nelopab  5572  0nelxp  5719  0xp  5784  nrelv  5810  dm0  5931  cnv0  6160  co02  6280  nlim0  6443  snsn0non  6509  imadif  6650  0fv  6950  poxp2  8168  poseq  8183  tz7.44lem1  8445  nlim1  8527  nlim2  8528  sdom0  9148  canth2  9170  snnen2o  9273  1sdom2  9276  canthp1lem2  10693  pwxpndom2  10705  adderpq  10996  mulerpq  10997  0ncn  11173  ax1ne0  11200  inelr  12256  xrltnr  13161  fzouzdisj  13735  lsw0  14603  eirr  16241  ruc  16279  aleph1re  16281  sqrt2irr  16285  n2dvds1  16405  n2dvds3  16408  sadc0  16491  1nprm  16716  join0  18450  meet0  18451  smndex1n0mnd  18925  nsmndex1  18926  smndex2dnrinv  18928  odhash  19592  cnfldfun  21378  cnfldfunOLD  21391  zringndrg  21479  zfbas  23904  ustn0  24229  zclmncvs  25182  lhop  26055  dvrelog  26679  nosgnn0  27703  sltsolem1  27720  addsrid  27997  muls01  28138  mulsrid  28139  axlowdimlem13  28969  ntrl2v2e  30177  konigsberglem4  30274  avril1  30482  helloworld  30484  topnfbey  30488  vsfval  30652  dmadjrnb  31925  xrge00  33017  esumrnmpt2  34069  measvuni  34215  sibf0  34336  ballotlem4  34501  signswch  34576  satf0n0  35383  fmlaomn0  35395  gonan0  35397  goaln0  35398  fmla0disjsuc  35403  elpotr  35782  dfon2lem7  35790  linedegen  36144  nmotru  36409  limsucncmpi  36446  bj-ru1  36944  bj-0nel1  36954  bj-inftyexpitaudisj  37206  bj-pinftynminfty  37228  finxp0  37392  poimirlem30  37657  coss0  38480  epnsymrel  38563  diophren  42824  notbicom  45170  rexanuz2nf  45503  stoweidlem44  46059  fourierdlem62  46183  salexct2  46354  aisbnaxb  46923  dandysum2p2e4  47010  iota0ndef  47051  aiota0ndef  47109  257prm  47548  fmtno4nprmfac193  47561  139prmALT  47583  31prm  47584  127prm  47586  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  usgrexmpl2trifr  47996  0nodd  48086  2nodd  48088  1neven  48154  2zrngnring  48174  ex-gt  49247  alsi-no-surprise  49315