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  2856  nemtbir  3029  ru  3727  ruOLD  3728  pssirr  4044  noel  4279  vn0  4286  uni0  4879  iun0  5005  0iun  5006  br0  5135  vprc  5252  iin0  5299  nfnid  5312  opelopabsb  5478  0nelopab  5513  0nelxp  5658  nrelv  5749  dm0  5869  cnv0  6097  cnv0OLD  6098  co02  6219  nlim0  6377  snsn0non  6443  imadif  6576  0fv  6875  poxp2  8086  poseq  8101  tz7.44lem1  8337  nlim1  8417  nlim2  8418  sdom0  9040  canth2  9061  snnen2o  9148  1sdom2  9151  canthp1lem2  10567  pwxpndom2  10579  adderpq  10870  mulerpq  10871  0ncn  11047  ax1ne0  11074  inelr  12140  xrltnr  13061  fzouzdisj  13641  lsw0  14518  eirr  16163  ruc  16201  aleph1re  16203  sqrt2irr  16207  n2dvds1  16328  n2dvds3  16331  sadc0  16414  1nprm  16639  join0  18360  meet0  18361  smndex1n0mnd  18874  nsmndex1  18875  smndex2dnrinv  18877  odhash  19540  cnfldfun  21358  cnfldfunOLD  21371  zringndrg  21458  zfbas  23871  ustn0  24196  zclmncvs  25125  lhop  25993  dvrelog  26614  nosgnn0  27636  ltssolem1  27653  addsrid  27970  muls01  28118  mulsrid  28119  axlowdimlem13  29037  ntrl2v2e  30243  konigsberglem4  30340  avril1  30548  helloworld  30550  topnfbey  30554  vsfval  30719  dmadjrnb  31992  xrge00  33089  domnprodeq0  33352  esumrnmpt2  34228  measvuni  34374  sibf0  34494  ballotlem4  34659  signswch  34721  satf0n0  35576  fmlaomn0  35588  gonan0  35590  goaln0  35591  fmla0disjsuc  35596  elpotr  35977  dfon2lem7  35985  linedegen  36341  nmotru  36606  limsucncmpi  36643  mh-inf3sn  36740  bj-ru1  37266  bj-0nel1  37276  bj-inftyexpitaudisj  37535  bj-pinftynminfty  37557  finxp0  37721  poimirlem30  37985  coss0  38904  epnsymrel  38981  sn-inelr  42946  diophren  43259  permaxnul  45453  permaxinf2lem  45457  notbicom  45613  rexanuz2nf  45938  stoweidlem44  46490  fourierdlem62  46614  salexct2  46785  chnerlem1  47328  aisbnaxb  47371  dandysum2p2e4  47458  iota0ndef  47499  aiota0ndef  47557  257prm  48036  fmtno4nprmfac193  48049  139prmALT  48071  31prm  48072  127prm  48074  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  usgrexmpl2trifr  48525  0nodd  48658  2nodd  48660  1neven  48726  2zrngnring  48746  ex-gt  50215  alsi-no-surprise  50283