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  1554  eqneltri  2853  nemtbir  3028  ru  3763  ruOLD  3764  pssirr  4078  noel  4313  iun0  5038  0iun  5039  br0  5168  vprc  5285  iin0  5332  nfnid  5345  opelopabsb  5505  0nelopab  5542  0nelxp  5688  0xp  5753  nrelv  5779  dm0  5900  cnv0  6129  co02  6249  nlim0  6412  snsn0non  6478  imadif  6619  0fv  6919  poxp2  8140  poseq  8155  tz7.44lem1  8417  nlim1  8499  nlim2  8500  sdom0  9120  canth2  9142  snnen2o  9243  1sdom2  9246  canthp1lem2  10665  pwxpndom2  10677  adderpq  10968  mulerpq  10969  0ncn  11145  ax1ne0  11172  inelr  12228  xrltnr  13133  fzouzdisj  13710  lsw0  14581  eirr  16221  ruc  16259  aleph1re  16261  sqrt2irr  16265  n2dvds1  16385  n2dvds3  16388  sadc0  16471  1nprm  16696  join0  18413  meet0  18414  smndex1n0mnd  18888  nsmndex1  18889  smndex2dnrinv  18891  odhash  19553  cnfldfun  21327  cnfldfunOLD  21340  zringndrg  21427  zfbas  23832  ustn0  24157  zclmncvs  25098  lhop  25971  dvrelog  26596  nosgnn0  27620  sltsolem1  27637  addsrid  27914  muls01  28055  mulsrid  28056  axlowdimlem13  28879  ntrl2v2e  30085  konigsberglem4  30182  avril1  30390  helloworld  30392  topnfbey  30396  vsfval  30560  dmadjrnb  31833  xrge00  32953  esumrnmpt2  34045  measvuni  34191  sibf0  34312  ballotlem4  34477  signswch  34539  satf0n0  35346  fmlaomn0  35358  gonan0  35360  goaln0  35361  fmla0disjsuc  35366  elpotr  35745  dfon2lem7  35753  linedegen  36107  nmotru  36372  limsucncmpi  36409  bj-ru1  36907  bj-0nel1  36917  bj-inftyexpitaudisj  37169  bj-pinftynminfty  37191  finxp0  37355  poimirlem30  37620  coss0  38443  epnsymrel  38526  diophren  42783  permaxnul  44981  permaxinf2lem  44985  notbicom  45137  rexanuz2nf  45467  stoweidlem44  46021  fourierdlem62  46145  salexct2  46316  aisbnaxb  46888  dandysum2p2e4  46975  iota0ndef  47016  aiota0ndef  47074  257prm  47523  fmtno4nprmfac193  47536  139prmALT  47558  31prm  47559  127prm  47561  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  usgrexmpl2trifr  47989  0nodd  48093  2nodd  48095  1neven  48161  2zrngnring  48181  ex-gt  49540  alsi-no-surprise  49608