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  2848  nemtbir  3022  ru  3754  ruOLD  3755  pssirr  4069  noel  4304  iun0  5029  0iun  5030  br0  5159  vprc  5273  iin0  5320  nfnid  5333  opelopabsb  5493  0nelopab  5530  0nelxp  5675  0xp  5740  nrelv  5766  dm0  5887  cnv0  6116  co02  6236  nlim0  6395  snsn0non  6462  imadif  6603  0fv  6905  poxp2  8125  poseq  8140  tz7.44lem1  8376  nlim1  8456  nlim2  8457  sdom0  9079  canth2  9100  snnen2o  9191  1sdom2  9194  canthp1lem2  10613  pwxpndom2  10625  adderpq  10916  mulerpq  10917  0ncn  11093  ax1ne0  11120  inelr  12183  xrltnr  13086  fzouzdisj  13663  lsw0  14537  eirr  16180  ruc  16218  aleph1re  16220  sqrt2irr  16224  n2dvds1  16345  n2dvds3  16348  sadc0  16431  1nprm  16656  join0  18371  meet0  18372  smndex1n0mnd  18846  nsmndex1  18847  smndex2dnrinv  18849  odhash  19511  cnfldfun  21285  cnfldfunOLD  21298  zringndrg  21385  zfbas  23790  ustn0  24115  zclmncvs  25055  lhop  25928  dvrelog  26553  nosgnn0  27577  sltsolem1  27594  addsrid  27878  muls01  28022  mulsrid  28023  axlowdimlem13  28888  ntrl2v2e  30094  konigsberglem4  30191  avril1  30399  helloworld  30401  topnfbey  30405  vsfval  30569  dmadjrnb  31842  xrge00  32960  esumrnmpt2  34065  measvuni  34211  sibf0  34332  ballotlem4  34497  signswch  34559  satf0n0  35372  fmlaomn0  35384  gonan0  35386  goaln0  35387  fmla0disjsuc  35392  elpotr  35776  dfon2lem7  35784  linedegen  36138  nmotru  36403  limsucncmpi  36440  bj-ru1  36938  bj-0nel1  36948  bj-inftyexpitaudisj  37200  bj-pinftynminfty  37222  finxp0  37386  poimirlem30  37651  coss0  38477  epnsymrel  38560  sn-inelr  42482  diophren  42808  permaxnul  45005  permaxinf2lem  45009  notbicom  45166  rexanuz2nf  45495  stoweidlem44  46049  fourierdlem62  46173  salexct2  46344  aisbnaxb  46916  dandysum2p2e4  47003  iota0ndef  47044  aiota0ndef  47102  257prm  47566  fmtno4nprmfac193  47579  139prmALT  47601  31prm  47602  127prm  47604  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  usgrexmpl2trifr  48032  0nodd  48162  2nodd  48164  1neven  48230  2zrngnring  48250  ex-gt  49721  alsi-no-surprise  49789