Theorem mtbir 322

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 223	. 2 ⊢ (𝜓 ↔ 𝜑)
4	1, 3	mtbi 321	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   ↔ wb 205

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 206

This theorem is referenced by:  3pm3.2ni  1484  fal  1548  eqneltri  2845  nemtbir  3028  ru  3774  ruOLD  3775  pssirr  4099  indifdirOLD  4287  noel  4333  noelOLD  4334  iun0  5070  0iun  5071  br0  5202  vprc  5320  iin0  5366  nfnid  5379  opelopabsb  5536  0nelopab  5573  0nelxp  5716  0xp  5780  nrelv  5806  dm0  5927  cnv0  6152  co02  6271  nlim0  6435  snsn0non  6501  imadif  6643  0fv  6945  poxp2  8157  poseq  8172  tz7.44lem1  8435  nlim1  8519  nlim2  8520  sdom0  9146  canth2  9168  snnen2o  9271  1sdom2  9274  canthp1lem2  10696  pwxpndom2  10708  adderpq  10999  mulerpq  11000  0ncn  11176  ax1ne0  11203  inelr  12254  xrltnr  13153  fzouzdisj  13722  lsw0  14573  eirr  16207  ruc  16245  aleph1re  16247  sqrt2irr  16251  n2dvds1  16370  n2dvds3  16373  sadc0  16454  1nprm  16680  join0  18430  meet0  18431  smndex1n0mnd  18902  nsmndex1  18903  smndex2dnrinv  18905  odhash  19572  cnfldfun  21357  cnfldfunOLD  21370  zringndrg  21458  zfbas  23891  ustn0  24216  zclmncvs  25167  lhop  26040  dvrelog  26664  nosgnn0  27688  sltsolem1  27705  addsrid  27978  muls01  28113  mulsrid  28114  axlowdimlem13  28888  ntrl2v2e  30091  konigsberglem4  30188  avril1  30396  helloworld  30398  topnfbey  30402  vsfval  30566  dmadjrnb  31839  xrge00  32895  esumrnmpt2  33901  measvuni  34047  sibf0  34168  ballotlem4  34332  signswch  34407  satf0n0  35206  fmlaomn0  35218  gonan0  35220  goaln0  35221  fmla0disjsuc  35226  elpotr  35605  dfon2lem7  35613  linedegen  35967  nmotru  36120  limsucncmpi  36157  bj-ru1  36650  bj-0nel1  36660  bj-inftyexpitaudisj  36912  bj-pinftynminfty  36934  finxp0  37098  poimirlem30  37351  coss0  38177  epnsymrel  38260  diophren  42470  notbicom  44771  rexanuz2nf  45108  stoweidlem44  45665  fourierdlem62  45789  salexct2  45960  aisbnaxb  46526  dandysum2p2e4  46613  iota0ndef  46654  aiota0ndef  46710  257prm  47133  fmtno4nprmfac193  47146  139prmALT  47168  31prm  47169  127prm  47171  nnsum4primeseven  47372  nnsum4primesevenALTV  47373  0nodd  47547  2nodd  47549  1neven  47615  2zrngnring  47635  ex-gt  48474  alsi-no-surprise  48544