Theorem mtbir 322

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

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  fal  1553  eqneltri  2832  nemtbir  3039  ru  3710  pssirr  4031  indifdirOLD  4216  noel  4261  noelOLD  4262  iun0  4987  0iun  4988  br0  5119  vprc  5234  iin0  5279  nfnid  5293  opelopabsb  5436  0nelopab  5471  0nelxp  5614  0xp  5675  nrelv  5699  dm0  5818  cnv0  6033  co02  6153  nlim0  6309  snsn0non  6370  imadif  6502  0fv  6795  tz7.44lem1  8207  canth2  8866  canthp1lem2  10340  pwxpndom2  10352  adderpq  10643  mulerpq  10644  0ncn  10820  ax1ne0  10847  inelr  11893  xrltnr  12784  fzouzdisj  13351  lsw0  14196  eirr  15842  ruc  15880  aleph1re  15882  sqrt2irr  15886  n2dvds1  16005  n2dvds3  16008  sadc0  16089  1nprm  16312  join0  18038  meet0  18039  smndex1n0mnd  18466  nsmndex1  18467  smndex2dnrinv  18469  odhash  19094  cnfldfunALT  20523  zringndrg  20602  zfbas  22955  ustn0  23280  zclmncvs  24217  lhop  25085  dvrelog  25697  axlowdimlem13  27225  ntrl2v2e  28423  konigsberglem4  28520  avril1  28728  helloworld  28730  topnfbey  28734  vsfval  28896  dmadjrnb  30169  xrge00  31197  esumrnmpt2  31936  measvuni  32082  sibf0  32201  ballotlem4  32365  signswch  32440  bnj521  32616  satf0n0  33240  fmlaomn0  33252  gonan0  33254  goaln0  33255  fmla0disjsuc  33260  3pm3.2ni  33558  elpotr  33663  dfon2lem7  33671  poxp2  33717  poseq  33729  nosgnn0  33788  sltsolem1  33805  addsid1  34054  linedegen  34372  nmotru  34524  subsym1  34543  limsucncmpi  34561  bj-ru1  35059  bj-0nel1  35070  bj-inftyexpitaudisj  35303  bj-pinftynminfty  35325  finxp0  35489  poimirlem30  35734  coss0  36524  epnsymrel  36603  diophren  40551  stoweidlem44  43475  fourierdlem62  43599  salexct2  43768  aisbnaxb  44293  dandysum2p2e4  44380  iota0ndef  44420  aiota0ndef  44476  257prm  44901  fmtno4nprmfac193  44914  139prmALT  44936  31prm  44937  127prm  44939  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  0nodd  45252  2nodd  45254  1neven  45378  2zrngnring  45398  ex-gt  46316  alsi-no-surprise  46386