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  2885  nemtbir  3057  ru  3746  pssirrOLD  4061  noel  4294  vn0  4301  vn0OLD  4302  uni0  4906  iun0  5031  0iun  5032  br0  5165  vprcOLD  5289  iin0  5338  nfnid  5351  opelopabsb  5519  0nelopab  5555  0nelxp  5700  nrelvOLD  5792  cnv0  5874  cnv0OLD  5875  dm0  5915  co02  6267  nlim0  6428  snsn0non  6494  imadif  6627  0fv  6929  poxp2  8148  poseq  8163  tz7.44lem1  8401  nlim1  8483  nlim2  8484  sdom0  9107  canth2  9128  snnen2o  9215  1sdom2  9218  canthp1lem2  10656  pwxpndom2  10668  adderpq  10959  mulerpq  10960  0ncn  11136  ax1ne0  11163  inelr  12226  xrltnr  13162  fzouzdisj  13743  lsw0  14622  eirr  16286  ruc  16324  aleph1re  16326  sqrt2irr  16330  n2dvds1  16451  n2dvds3  16454  sadc0  16537  1nprm  16762  join0  18484  meet0  18485  smndex1n0mnd  19005  nsmndex1  19006  smndex2dnrinv  19008  odhash  19675  cnfldfun  21573  zringndrg  21655  zfbas  24090  ustn0  24415  zclmncvs  25344  lhop  26212  dvrelog  26839  nosgnn0  27859  ltssolem1  27876  addsrid  28194  muls01  28342  mulsrid  28343  axlowdimlem13  29341  ntrl2v2e  30546  konigsberglem4  30643  avril1  30851  helloworld  30853  topnfbey  30857  nowisdomv  30862  vsfval  31022  dmadjrnb  32295  xrge00  33365  domnprodeq0  33630  esumrnmpt2  34489  measvuni  34636  sibf0  34756  ballotlem4  34921  signswch  34980  satf0n0  35891  fmlaomn0  35903  gonan0  35905  goaln0  35906  fmla0disjsuc  35911  elpotr  36292  dfon2lem7  36300  linedegen  36656  nmotru  36960  limsucncmpi  36997  mh-inf3sn  37094  bj-ru1  37620  bj-0nel1  37630  bj-inftyexpitaudisj  37890  bj-pinftynminfty  37912  finxp0  38078  poimirlem30  38342  coss0  39259  epnsymrel  39336  sn-inelr  43302  diophren  43581  permaxnul  45758  permaxinf2lem  45762  notbicom  45924  rexanuz2nf  46247  stoweidlem44  46799  fourierdlem62  46923  salexct2  47094  chnerlem1  47639  aisbnaxb  47689  dandysum2p2e4  47776  iota0ndef  47817  aiota0ndef  47875  257prm  48354  fmtno4nprmfac193  48367  139prmALT  48389  31prm  48390  127prm  48392  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  usgrexmpl2trifr  48843  0nodd  48976  2nodd  48978  1neven  49044  2zrngnring  49064  ex-gt  50547  als-no-surprise  50625  rals-no-surprise  50626