Theorem mtbir 323

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  3pm3.2ni  1491  fal  1556  eqneltri  2855  nemtbir  3028  ru  3726  ruOLD  3727  pssirr  4043  noel  4278  vn0  4285  uni0  4878  iun0  5004  0iun  5005  br0  5134  vprcOLD  5256  iin0  5304  nfnid  5317  opelopabsb  5485  0nelopab  5520  0nelxp  5665  nrelv  5756  dm0  5875  cnv0  6103  cnv0OLD  6104  co02  6225  nlim0  6383  snsn0non  6449  imadif  6582  0fv  6881  poxp2  8093  poseq  8108  tz7.44lem1  8344  nlim1  8424  nlim2  8425  sdom0  9047  canth2  9068  snnen2o  9155  1sdom2  9158  canthp1lem2  10576  pwxpndom2  10588  adderpq  10879  mulerpq  10880  0ncn  11056  ax1ne0  11083  inelr  12149  xrltnr  13070  fzouzdisj  13650  lsw0  14527  eirr  16172  ruc  16210  aleph1re  16212  sqrt2irr  16216  n2dvds1  16337  n2dvds3  16340  sadc0  16423  1nprm  16648  join0  18369  meet0  18370  smndex1n0mnd  18883  nsmndex1  18884  smndex2dnrinv  18886  odhash  19549  cnfldfun  21366  zringndrg  21448  zfbas  23861  ustn0  24186  zclmncvs  25115  lhop  25983  dvrelog  26601  nosgnn0  27622  ltssolem1  27639  addsrid  27956  muls01  28104  mulsrid  28105  axlowdimlem13  29023  ntrl2v2e  30228  konigsberglem4  30325  avril1  30533  helloworld  30535  topnfbey  30539  nowisdomv  30544  vsfval  30704  dmadjrnb  31977  xrge00  33074  domnprodeq0  33337  esumrnmpt2  34212  measvuni  34358  sibf0  34478  ballotlem4  34643  signswch  34705  satf0n0  35560  fmlaomn0  35572  gonan0  35574  goaln0  35575  fmla0disjsuc  35580  elpotr  35961  dfon2lem7  35969  linedegen  36325  nmotru  36590  limsucncmpi  36627  mh-inf3sn  36724  bj-ru1  37250  bj-0nel1  37260  bj-inftyexpitaudisj  37519  bj-pinftynminfty  37541  finxp0  37707  poimirlem30  37971  coss0  38890  epnsymrel  38967  sn-inelr  42932  diophren  43241  permaxnul  45435  permaxinf2lem  45439  notbicom  45595  rexanuz2nf  45920  stoweidlem44  46472  fourierdlem62  46596  salexct2  46767  chnerlem1  47312  aisbnaxb  47359  dandysum2p2e4  47446  iota0ndef  47487  aiota0ndef  47545  257prm  48024  fmtno4nprmfac193  48037  139prmALT  48059  31prm  48060  127prm  48062  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  usgrexmpl2trifr  48513  0nodd  48646  2nodd  48648  1neven  48714  2zrngnring  48734  ex-gt  50203  alsi-no-surprise  50271