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  1490  fal  1555  eqneltri  2855  nemtbir  3028  ru  3738  ruOLD  3739  pssirr  4055  noel  4290  vn0  4297  uni0  4891  iun0  5017  0iun  5018  br0  5147  vprc  5260  iin0  5307  nfnid  5320  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  8085  poseq  8100  tz7.44lem1  8336  nlim1  8416  nlim2  8417  sdom0  9037  canth2  9058  snnen2o  9145  1sdom2  9148  canthp1lem2  10564  pwxpndom2  10576  adderpq  10867  mulerpq  10868  0ncn  11044  ax1ne0  11071  inelr  12135  xrltnr  13033  fzouzdisj  13611  lsw0  14488  eirr  16130  ruc  16168  aleph1re  16170  sqrt2irr  16174  n2dvds1  16295  n2dvds3  16298  sadc0  16381  1nprm  16606  join0  18326  meet0  18327  smndex1n0mnd  18837  nsmndex1  18838  smndex2dnrinv  18840  odhash  19503  cnfldfun  21323  cnfldfunOLD  21336  zringndrg  21423  zfbas  23840  ustn0  24165  zclmncvs  25104  lhop  25977  dvrelog  26602  nosgnn0  27626  ltssolem1  27643  addsrid  27960  muls01  28108  mulsrid  28109  axlowdimlem13  29027  ntrl2v2e  30233  konigsberglem4  30330  avril1  30538  helloworld  30540  topnfbey  30544  vsfval  30708  dmadjrnb  31981  xrge00  33096  domnprodeq0  33358  esumrnmpt2  34225  measvuni  34371  sibf0  34491  ballotlem4  34656  signswch  34718  satf0n0  35572  fmlaomn0  35584  gonan0  35586  goaln0  35587  fmla0disjsuc  35592  elpotr  35973  dfon2lem7  35981  linedegen  36337  nmotru  36602  limsucncmpi  36639  bj-ru1  37144  bj-0nel1  37154  bj-inftyexpitaudisj  37410  bj-pinftynminfty  37432  finxp0  37596  poimirlem30  37851  coss0  38742  epnsymrel  38819  sn-inelr  42742  diophren  43055  permaxnul  45249  permaxinf2lem  45253  notbicom  45409  rexanuz2nf  45736  stoweidlem44  46288  fourierdlem62  46412  salexct2  46583  chnerlem1  47126  aisbnaxb  47157  dandysum2p2e4  47244  iota0ndef  47285  aiota0ndef  47343  257prm  47807  fmtno4nprmfac193  47820  139prmALT  47842  31prm  47843  127prm  47845  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  usgrexmpl2trifr  48283  0nodd  48416  2nodd  48418  1neven  48484  2zrngnring  48504  ex-gt  49973  alsi-no-surprise  50041