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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  fal  1553  eqneltri  2833  nemtbir  3041  ru  3716  pssirr  4036  indifdirOLD  4220  noel  4265  noelOLD  4266  iun0  4992  0iun  4993  br0  5124  vprc  5240  iin0  5285  nfnid  5299  opelopabsb  5444  0nelopab  5481  0nelxp  5624  0xp  5686  nrelv  5712  dm0  5832  cnv0  6049  co02  6168  nlim0  6328  snsn0non  6389  imadif  6525  0fv  6822  tz7.44lem1  8245  nlim1  8328  nlim2  8329  sdom0  8904  canth2  8926  snnen2o  9035  canthp1lem2  10418  pwxpndom2  10430  adderpq  10721  mulerpq  10722  0ncn  10898  ax1ne0  10925  inelr  11972  xrltnr  12864  fzouzdisj  13432  lsw0  14277  eirr  15923  ruc  15961  aleph1re  15963  sqrt2irr  15967  n2dvds1  16086  n2dvds3  16089  sadc0  16170  1nprm  16393  join0  18132  meet0  18133  smndex1n0mnd  18560  nsmndex1  18561  smndex2dnrinv  18563  odhash  19188  cnfldfun  20618  zringndrg  20699  zfbas  23056  ustn0  23381  zclmncvs  24321  lhop  25189  dvrelog  25801  axlowdimlem13  27331  ntrl2v2e  28531  konigsberglem4  28628  avril1  28836  helloworld  28838  topnfbey  28842  vsfval  29004  dmadjrnb  30277  xrge00  31304  esumrnmpt2  32045  measvuni  32191  sibf0  32310  ballotlem4  32474  signswch  32549  bnj521  32725  satf0n0  33349  fmlaomn0  33361  gonan0  33363  goaln0  33364  fmla0disjsuc  33369  3pm3.2ni  33665  elpotr  33766  dfon2lem7  33774  poxp2  33799  poseq  33811  nosgnn0  33870  sltsolem1  33887  addsid1  34136  linedegen  34454  nmotru  34606  subsym1  34625  limsucncmpi  34643  bj-ru1  35141  bj-0nel1  35152  bj-inftyexpitaudisj  35385  bj-pinftynminfty  35407  finxp0  35571  poimirlem30  35816  coss0  36604  epnsymrel  36683  diophren  40642  stoweidlem44  43592  fourierdlem62  43716  salexct2  43885  aisbnaxb  44417  dandysum2p2e4  44504  iota0ndef  44544  aiota0ndef  44600  257prm  45024  fmtno4nprmfac193  45037  139prmALT  45059  31prm  45060  127prm  45062  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  0nodd  45375  2nodd  45377  1neven  45501  2zrngnring  45521  ex-gt  46441  alsi-no-surprise  46511