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  1518  fal  1583  eqneltri  2879  nemtbir  3051  ru  3737  pssirrOLD  4031  noel  4283  vn0  4290  vn0OLD  4291  uni0  4895  iun0  5019  0iun  5020  br0  5153  vprcOLD  5274  iin0  5323  nfnid  5336  opelopabsb  5503  0nelopab  5539  0nelxp  5684  nrelvOLD  5777  cnv0  5860  cnv0OLD  5861  dm0  5901  co02  6262  nlim0  6423  snsn0non  6489  imadif  6625  0fv  6927  poxp2  8163  poseq  8178  tz7.44lem1  8417  nlim1  8501  nlim2  8502  sdom0  9132  canth2  9153  snnen2o  9240  1sdom2  9243  canthp1lem2  10742  pwxpndom2  10754  adderpq  11045  mulerpq  11046  0ncn  11222  ax1ne0  11249  inelr  12314  xrltnr  13252  fzouzdisj  13834  lsw0  14714  eirr  16379  ruc  16417  aleph1re  16419  sqrt2irr  16423  n2dvds1  16544  n2dvds3  16547  sadc0  16630  1nprm  16860  join0  18583  meet0  18584  smndex1n0mnd  19117  nsmndex1  19118  smndex2dnrinv  19120  degenmgmnfn  19142  degenmgm2nfun  19145  odhash  19794  cnfldfun  21698  zringndrg  21780  zfbas  24221  ustn0  24546  zclmncvs  25475  lhop  26342  dvrelog  26971  nosgnn0  28021  ltssolem1  28038  addsrid  28356  muls01  28504  mulsrid  28505  axlowdimlem13  29538  ntrl2v2e  30765  konigsberglem4  30862  avril1  31070  helloworld  31072  topnfbey  31076  nowisdomv  31081  vsfval  31241  dmadjrnb  32514  xrge00  33622  domnprodeq0  33887  esumrnmpt2  34747  measvuni  34894  sibf0  35013  ballotlem4  35178  signswch  35237  satf0n0  36230  fmlaomn0  36242  gonan0  36244  goaln0  36245  fmla0disjsuc  36250  elpotr  36636  dfon2lem7  36644  linedegen  37001  nmotru  37289  limsucncmpi  37326  mh-inf3sn  37423  bj-ru1  37949  bj-0nel1  37959  bj-inftyexpitaudisj  38220  bj-pinftynminfty  38242  finxp0  38408  poimirlem30  38662  coss0  39595  epnsymrel  39672  sn-inelr  43645  diophren  43914  permaxnul  46092  permaxinf2lem  46096  notbicom  46274  rexanuz2nf  46596  stoweidlem44  47148  fourierdlem62  47272  salexct2  47443  chnerlem1  47986  aisbnaxb  48075  dandysum2p2e4  48162  iota0ndef  48203  aiota0ndef  48261  257prm  48740  fmtno4nprmfac193  48753  139prmALT  48775  31prm  48776  127prm  48778  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  usgrexmpl2trifr  49229  0nodd  49361  2nodd  49363  1neven  49429  2zrngnring  49449  ex-gt  50990  als-no-surprise  51071  rals-no-surprise  51072