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  2847  nemtbir  3021  ru  3742  ruOLD  3743  pssirr  4056  noel  4291  iun0  5014  0iun  5015  br0  5144  vprc  5257  iin0  5304  nfnid  5317  opelopabsb  5477  0nelopab  5512  0nelxp  5657  0xp  5722  nrelv  5747  dm0  5867  cnv0  6093  co02  6213  nlim0  6371  snsn0non  6437  imadif  6570  0fv  6868  poxp2  8083  poseq  8098  tz7.44lem1  8334  nlim1  8414  nlim2  8415  sdom0  9033  canth2  9054  snnen2o  9144  1sdom2  9147  canthp1lem2  10566  pwxpndom2  10578  adderpq  10869  mulerpq  10870  0ncn  11046  ax1ne0  11073  inelr  12136  xrltnr  13039  fzouzdisj  13616  lsw0  14490  eirr  16132  ruc  16170  aleph1re  16172  sqrt2irr  16176  n2dvds1  16297  n2dvds3  16300  sadc0  16383  1nprm  16608  join0  18327  meet0  18328  smndex1n0mnd  18804  nsmndex1  18805  smndex2dnrinv  18807  odhash  19471  cnfldfun  21293  cnfldfunOLD  21306  zringndrg  21393  zfbas  23799  ustn0  24124  zclmncvs  25064  lhop  25937  dvrelog  26562  nosgnn0  27586  sltsolem1  27603  addsrid  27894  muls01  28038  mulsrid  28039  axlowdimlem13  28917  ntrl2v2e  30120  konigsberglem4  30217  avril1  30425  helloworld  30427  topnfbey  30431  vsfval  30595  dmadjrnb  31868  xrge00  32981  esumrnmpt2  34037  measvuni  34183  sibf0  34304  ballotlem4  34469  signswch  34531  satf0n0  35353  fmlaomn0  35365  gonan0  35367  goaln0  35368  fmla0disjsuc  35373  elpotr  35757  dfon2lem7  35765  linedegen  36119  nmotru  36384  limsucncmpi  36421  bj-ru1  36919  bj-0nel1  36929  bj-inftyexpitaudisj  37181  bj-pinftynminfty  37203  finxp0  37367  poimirlem30  37632  coss0  38458  epnsymrel  38541  sn-inelr  42463  diophren  42789  permaxnul  44985  permaxinf2lem  44989  notbicom  45146  rexanuz2nf  45475  stoweidlem44  46029  fourierdlem62  46153  salexct2  46324  aisbnaxb  46899  dandysum2p2e4  46986  iota0ndef  47027  aiota0ndef  47085  257prm  47549  fmtno4nprmfac193  47562  139prmALT  47584  31prm  47585  127prm  47587  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  usgrexmpl2trifr  48025  0nodd  48158  2nodd  48160  1neven  48226  2zrngnring  48246  ex-gt  49717  alsi-no-surprise  49785