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  1512  fal  1577  eqneltri  2884  nemtbir  3056  ru  3746  pssirrOLD  4060  noel  4293  vn0  4300  uni0  4896  iun0  5021  0iun  5022  br0  5153  vprcOLD  5275  iin0  5323  nfnid  5336  opelopabsb  5504  0nelopab  5540  0nelxp  5685  nrelvOLD  5777  cnv0  5859  cnv0OLD  5860  dm0  5900  co02  6251  nlim0  6410  snsn0non  6476  imadif  6609  0fv  6912  poxp2  8127  poseq  8142  tz7.44lem1  8380  nlim1  8462  nlim2  8463  sdom0  9085  canth2  9106  snnen2o  9193  1sdom2  9196  canthp1lem2  10626  pwxpndom2  10638  adderpq  10929  mulerpq  10930  0ncn  11106  ax1ne0  11133  inelr  12196  xrltnr  13132  fzouzdisj  13712  lsw0  14590  eirr  16249  ruc  16287  aleph1re  16289  sqrt2irr  16293  n2dvds1  16414  n2dvds3  16417  sadc0  16500  1nprm  16725  join0  18447  meet0  18448  smndex1n0mnd  18962  nsmndex1  18963  smndex2dnrinv  18965  odhash  19632  cnfldfun  21493  zringndrg  21575  zfbas  24010  ustn0  24335  zclmncvs  25264  lhop  26132  dvrelog  26756  nosgnn0  27776  ltssolem1  27793  addsrid  28111  muls01  28259  mulsrid  28260  axlowdimlem13  29209  ntrl2v2e  30414  konigsberglem4  30511  avril1  30719  helloworld  30721  topnfbey  30725  nowisdomv  30730  vsfval  30890  dmadjrnb  32163  xrge00  33242  domnprodeq0  33507  esumrnmpt2  34370  measvuni  34516  sibf0  34636  ballotlem4  34801  signswch  34860  satf0n0  35736  fmlaomn0  35748  gonan0  35750  goaln0  35751  fmla0disjsuc  35756  elpotr  36137  dfon2lem7  36145  linedegen  36501  nmotru  36776  limsucncmpi  36813  mh-inf3sn  36910  bj-ru1  37435  bj-0nel1  37445  bj-inftyexpitaudisj  37704  bj-pinftynminfty  37726  finxp0  37892  poimirlem30  38156  coss0  39075  epnsymrel  39152  sn-inelr  43116  diophren  43397  permaxnul  45576  permaxinf2lem  45580  notbicom  45742  rexanuz2nf  46065  stoweidlem44  46617  fourierdlem62  46741  salexct2  46912  chnerlem1  47457  aisbnaxb  47504  dandysum2p2e4  47591  iota0ndef  47632  aiota0ndef  47690  257prm  48169  fmtno4nprmfac193  48182  139prmALT  48204  31prm  48205  127prm  48207  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  usgrexmpl2trifr  48658  0nodd  48791  2nodd  48793  1neven  48859  2zrngnring  48879  ex-gt  50358  alsi-no-surprise  50426