Theorem mtbir 326

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

Syntax hints:  ¬ wn 3   ↔ wb 209

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 210

This theorem is referenced by:  fal  1552  eqneltri  2845  nemtbir  3046  ru  3695  pssirr  4006  indifdirOLD  4190  noel  4230  iun0  4950  0iun  4951  br0  5081  vprc  5185  iin0  5229  nfnid  5244  opelopabsb  5387  0nelxp  5558  0xp  5618  nrelv  5642  dm0  5761  cnv0  5971  co02  6090  nlim0  6227  snsn0non  6288  imadif  6419  0fv  6697  tz7.44lem1  8051  canth2  8692  canthp1lem2  10113  pwxpndom2  10125  adderpq  10416  mulerpq  10417  0ncn  10593  ax1ne0  10620  inelr  11664  xrltnr  12555  fzouzdisj  13122  lsw0  13964  eirr  15606  ruc  15644  aleph1re  15646  sqrt2irr  15650  n2dvds1  15769  n2dvds3  15772  sadc0  15853  1nprm  16075  meet0  17813  join0  17814  smndex1n0mnd  18143  nsmndex1  18144  smndex2dnrinv  18146  odhash  18766  cnfldfunALT  20179  zringndrg  20258  zfbas  22596  ustn0  22921  zclmncvs  23849  lhop  24715  dvrelog  25327  axlowdimlem13  26847  ntrl2v2e  28042  konigsberglem4  28139  avril1  28347  helloworld  28349  topnfbey  28353  vsfval  28515  dmadjrnb  29788  xrge00  30821  esumrnmpt2  31555  measvuni  31701  sibf0  31820  ballotlem4  31984  signswch  32059  bnj521  32235  satf0n0  32856  fmlaomn0  32868  gonan0  32870  goaln0  32871  fmla0disjsuc  32876  3pm3.2ni  33174  elpotr  33273  dfon2lem7  33281  poxp2  33345  poseq  33356  nosgnn0  33426  sltsolem1  33443  addsid1  33675  linedegen  33994  nmotru  34146  subsym1  34165  limsucncmpi  34183  bj-ru1  34659  bj-0nel1  34670  bj-inftyexpitaudisj  34900  bj-pinftynminfty  34922  bj-isrvec  34988  finxp0  35088  poimirlem30  35367  coss0  36159  epnsymrel  36238  diophren  40127  stoweidlem44  43052  fourierdlem62  43176  salexct2  43345  aisbnaxb  43870  dandysum2p2e4  43957  iota0ndef  43997  aiota0ndef  44020  257prm  44446  fmtno4nprmfac193  44459  139prmALT  44481  31prm  44482  127prm  44484  nnsum4primeseven  44685  nnsum4primesevenALTV  44686  0nodd  44797  2nodd  44799  1neven  44923  2zrngnring  44943  ex-gt  45645  alsi-no-surprise  45715