Theorem mtbir 324

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

Syntax hints:  ¬ wn 3   ↔ wb 207

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 208

This theorem is referenced by:  3pm3.2ni  1496  fal  1561  eqneltri  2859  nemtbir  3031  ru  3728  ruOLD  3729  pssirr  4041  noel  4273  vn0  4280  uni0  4873  iun0  4998  0iun  4999  br0  5128  vprcOLD  5250  iin0  5298  nfnid  5311  opelopabsb  5479  0nelopab  5514  0nelxp  5659  nrelv  5750  dm0  5869  cnv0  6097  cnv0OLD  6098  co02  6219  nlim0  6377  snsn0non  6443  imadif  6576  0fv  6875  poxp2  8090  poseq  8105  tz7.44lem1  8341  nlim1  8421  nlim2  8422  sdom0  9044  canth2  9065  snnen2o  9152  1sdom2  9155  canthp1lem2  10574  pwxpndom2  10586  adderpq  10877  mulerpq  10878  0ncn  11054  ax1ne0  11081  inelr  12147  xrltnr  13068  fzouzdisj  13648  lsw0  14525  eirr  16170  ruc  16208  aleph1re  16210  sqrt2irr  16214  n2dvds1  16335  n2dvds3  16338  sadc0  16421  1nprm  16646  join0  18367  meet0  18368  smndex1n0mnd  18881  nsmndex1  18882  smndex2dnrinv  18884  odhash  19547  cnfldfun  21368  zringndrg  21450  zfbas  23886  ustn0  24211  zclmncvs  25140  lhop  26008  dvrelog  26626  nosgnn0  27647  ltssolem1  27664  addsrid  27981  muls01  28129  mulsrid  28130  axlowdimlem13  29048  ntrl2v2e  30253  konigsberglem4  30350  avril1  30558  helloworld  30560  topnfbey  30564  nowisdomv  30569  vsfval  30729  dmadjrnb  32002  xrge00  33100  domnprodeq0  33364  esumrnmpt2  34259  measvuni  34405  sibf0  34525  ballotlem4  34690  signswch  34752  satf0n0  35613  fmlaomn0  35625  gonan0  35627  goaln0  35628  fmla0disjsuc  35633  elpotr  36014  dfon2lem7  36022  linedegen  36378  nmotru  36643  limsucncmpi  36680  mh-inf3sn  36777  bj-ru1  37303  bj-0nel1  37313  bj-inftyexpitaudisj  37572  bj-pinftynminfty  37594  finxp0  37760  poimirlem30  38024  coss0  38943  epnsymrel  39020  sn-inelr  42984  diophren  43265  permaxnul  45459  permaxinf2lem  45463  notbicom  45619  rexanuz2nf  45942  stoweidlem44  46494  fourierdlem62  46618  salexct2  46789  chnerlem1  47334  aisbnaxb  47381  dandysum2p2e4  47468  iota0ndef  47509  aiota0ndef  47567  257prm  48046  fmtno4nprmfac193  48059  139prmALT  48081  31prm  48082  127prm  48084  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  usgrexmpl2trifr  48535  0nodd  48668  2nodd  48670  1neven  48736  2zrngnring  48756  ex-gt  50225  alsi-no-surprise  50293