Theorem mtbir 314

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

Syntax hints:  ¬ wn 3   ↔ wb 197

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 198

This theorem is referenced by:  fal  1652  nemtbir  3084  ru  3643  pssirr  3916  indifdir  4096  noel  4131  iun0  4779  0iun  4780  br0  4904  vprc  5003  iin0  5042  nfnid  5056  opelopabsb  5191  0nelxp  5355  0xp  5412  nrelv  5457  dm0  5551  cnv0  5757  co02  5874  nlim0  6006  snsn0non  6066  imadif  6191  0fv  6454  snnexOLD  7204  iprc  7338  tfr2b  7735  tz7.44lem1  7744  tz7.48-3  7782  canth2  8359  pwcdadom  9330  canthp1lem2  9767  pwxpndom2  9779  adderpq  10070  mulerpq  10071  0ncn  10246  ax1ne0  10273  pnfnre  10373  mnfnre  10374  inelr  11302  xrltnr  12176  fzouzdisj  12735  lsw0  13571  fprodn0f  14949  eirr  15160  ruc  15199  aleph1re  15201  sqrt2irr  15206  sadc0  15402  1nprm  15617  3prm  15631  prmrec  15850  meet0  17349  join0  17350  odhash  18197  00lsp  19195  cnfldfunALT  19974  zringndrg  20053  zfbas  21921  ustn0  22245  zclmncvs  23168  lhop  24003  dvrelog  24607  axlowdimlem13  26058  ntrl2v2e  27341  konigsberglem4  27438  avril1  27660  helloworld  27662  topnfbey  27666  vsfval  27826  dmadjrnb  29103  xrge00  30021  esumrnmpt2  30465  measvuni  30612  sibf0  30731  ballotlem4  30895  signswch  30973  bnj521  31138  3pm3.2ni  31925  elpotr  32015  dfon2lem7  32023  poseq  32083  nosgnn0  32141  sltsolem1  32156  linedegen  32580  nmotru  32734  subsym1  32752  limsucncmpi  32770  bj-ru1  33250  bj-0nel1  33256  bj-pinftynrr  33432  bj-minftynrr  33436  bj-pinftynminfty  33437  finxp0  33550  poimirlem30  33758  coss0  34548  epnsymrel  34627  diophren  37884  eqneltri  39744  stoweidlem44  40745  fourierdlem62  40869  salexct2  41041  aisbnaxb  41565  dandysum2p2e4  41652  iota0ndef  41663  aiota0ndef  41684  257prm  42053  fmtno4nprmfac193  42066  139prmALT  42091  31prm  42092  127prm  42095  nnsum4primeseven  42268  nnsum4primesevenALTV  42269  0nodd  42383  2nodd  42385  1neven  42505  2zrngnring  42525  ex-gt  43045  alsi-no-surprise  43118