Theorem mtbir 325

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  fal  1551  eqneltri  2906  nemtbir  3112  ru  3771  pssirr  4077  indifdir  4260  noel  4296  noelOLD  4297  iun0  4985  0iun  4986  br0  5115  vprc  5219  iin0  5261  nfnid  5276  opelopabsb  5417  0nelxp  5589  0xp  5649  nrelv  5673  dm0  5790  cnv0  5999  co02  6113  nlim0  6249  snsn0non  6309  imadif  6438  0fv  6709  tz7.44lem1  8041  canth2  8670  canthp1lem2  10075  pwxpndom2  10087  adderpq  10378  mulerpq  10379  0ncn  10555  ax1ne0  10582  inelr  11628  xrltnr  12515  fzouzdisj  13074  lsw0  13917  eirr  15558  ruc  15596  aleph1re  15598  sqrt2irr  15602  n2dvds1  15717  n2dvds3  15721  sadc0  15803  1nprm  16023  meet0  17747  join0  17748  smndex1n0mnd  18077  nsmndex1  18078  smndex2dnrinv  18080  odhash  18699  cnfldfunALT  20558  zringndrg  20637  zfbas  22504  ustn0  22829  zclmncvs  23752  lhop  24613  dvrelog  25220  axlowdimlem13  26740  ntrl2v2e  27937  konigsberglem4  28034  avril1  28242  helloworld  28244  topnfbey  28248  vsfval  28410  dmadjrnb  29683  xrge00  30673  esumrnmpt2  31327  measvuni  31473  sibf0  31592  ballotlem4  31756  signswch  31831  bnj521  32007  satf0n0  32625  fmlaomn0  32637  gonan0  32639  goaln0  32640  fmla0disjsuc  32645  3pm3.2ni  32943  elpotr  33026  dfon2lem7  33034  poseq  33095  nosgnn0  33165  sltsolem1  33180  linedegen  33604  nmotru  33756  subsym1  33775  limsucncmpi  33793  bj-ru1  34257  bj-0nel1  34268  bj-inftyexpitaudisj  34490  bj-pinftynminfty  34512  bj-isrvec  34578  finxp0  34675  poimirlem30  34937  coss0  35734  epnsymrel  35813  diophren  39430  stoweidlem44  42349  fourierdlem62  42473  salexct2  42642  aisbnaxb  43167  dandysum2p2e4  43254  iota0ndef  43294  aiota0ndef  43315  257prm  43743  fmtno4nprmfac193  43756  139prmALT  43779  31prm  43780  127prm  43783  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  0nodd  44097  2nodd  44099  1neven  44223  2zrngnring  44243  ex-gt  44847  alsi-no-surprise  44917