Theorem mtbir 312

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

Syntax hints:  ¬ wn 3   ↔ wb 196

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 197

This theorem is referenced by:  fal  1638  nemtbir  3038  ru  3586  pssirr  3857  indifdir  4032  noel  4067  iun0  4710  0iun  4711  br0  4835  vprc  4931  iin0  4970  nfnid  5025  opelopabsb  5118  0nelxp  5283  0nelxpOLD  5284  0xp  5339  nrelv  5383  dm0  5477  cnv0  5676  co02  5793  nlim0  5926  snsn0non  5989  imadif  6113  0fv  6368  snnexOLD  7114  iprc  7248  tfr2b  7645  tz7.44lem1  7654  tz7.48-3  7692  canth2  8269  pwcdadom  9240  canthp1lem2  9677  pwxpndom2  9689  adderpq  9980  mulerpq  9981  0ncn  10156  ax1ne0  10183  pnfnre  10283  mnfnre  10284  inelr  11212  xrltnr  12158  fzouzdisj  12712  lsw0  13549  fprodn0f  14928  eirr  15139  ruc  15178  aleph1re  15180  sqrt2irr  15185  sadc0  15384  1nprm  15599  3prm  15613  prmrec  15833  meet0  17345  join0  17346  odhash  18196  00lsp  19194  cnfldfunALT  19974  zringndrg  20053  zfbas  21920  ustn0  22244  zclmncvs  23167  lhop  23999  dvrelog  24604  axlowdimlem13  26055  ntrl2v2e  27338  konigsberglem4  27435  avril1  27661  helloworld  27663  topnfbey  27667  vsfval  27828  dmadjrnb  29105  xrge00  30026  esumrnmpt2  30470  measvuni  30617  sibf0  30736  ballotlem4  30900  signswch  30978  bnj521  31143  3pm3.2ni  31932  elpotr  32022  dfon2lem7  32030  poseq  32090  nosgnn0  32148  sltsolem1  32163  linedegen  32587  mont  32745  subsym1  32763  limsucncmpi  32781  bj-ru1  33265  bj-0nel1  33271  bj-pinftynrr  33446  bj-minftynrr  33450  bj-pinftynminfty  33451  finxp0  33565  poimirlem30  33772  coss0  34571  epnsymrel  34650  diophren  37903  eqneltri  39767  stoweidlem44  40778  fourierdlem62  40902  salexct2  41074  aisbnaxb  41598  dandysum2p2e4  41685  257prm  42001  fmtno4nprmfac193  42014  139prmALT  42039  31prm  42040  127prm  42043  nnsum4primeseven  42216  nnsum4primesevenALTV  42217  0nodd  42338  2nodd  42340  1neven  42460  2zrngnring  42480  ex-gt  43000  alsi-no-surprise  43073