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  1486  fal  1550  eqneltri  2857  nemtbir  3035  ru  3788  ruOLD  3789  pssirr  4112  noel  4343  iun0  5066  0iun  5067  br0  5196  vprc  5320  iin0  5367  nfnid  5380  opelopabsb  5539  0nelopab  5576  0nelxp  5722  0xp  5786  nrelv  5812  dm0  5933  cnv0  6162  co02  6281  nlim0  6444  snsn0non  6510  imadif  6651  0fv  6950  poxp2  8166  poseq  8181  tz7.44lem1  8443  nlim1  8525  nlim2  8526  sdom0  9146  canth2  9168  snnen2o  9270  1sdom2  9273  canthp1lem2  10690  pwxpndom2  10702  adderpq  10993  mulerpq  10994  0ncn  11170  ax1ne0  11197  inelr  12253  xrltnr  13158  fzouzdisj  13731  lsw0  14599  eirr  16237  ruc  16275  aleph1re  16277  sqrt2irr  16281  n2dvds1  16401  n2dvds3  16404  sadc0  16487  1nprm  16712  join0  18462  meet0  18463  smndex1n0mnd  18937  nsmndex1  18938  smndex2dnrinv  18940  odhash  19606  cnfldfun  21395  cnfldfunOLD  21408  zringndrg  21496  zfbas  23919  ustn0  24244  zclmncvs  25195  lhop  26069  dvrelog  26693  nosgnn0  27717  sltsolem1  27734  addsrid  28011  muls01  28152  mulsrid  28153  axlowdimlem13  28983  ntrl2v2e  30186  konigsberglem4  30283  avril1  30491  helloworld  30493  topnfbey  30497  vsfval  30661  dmadjrnb  31934  xrge00  32999  esumrnmpt2  34048  measvuni  34194  sibf0  34315  ballotlem4  34479  signswch  34554  satf0n0  35362  fmlaomn0  35374  gonan0  35376  goaln0  35377  fmla0disjsuc  35382  elpotr  35762  dfon2lem7  35770  linedegen  36124  nmotru  36390  limsucncmpi  36427  bj-ru1  36925  bj-0nel1  36935  bj-inftyexpitaudisj  37187  bj-pinftynminfty  37209  finxp0  37373  poimirlem30  37636  coss0  38460  epnsymrel  38543  diophren  42800  notbicom  45107  rexanuz2nf  45442  stoweidlem44  45999  fourierdlem62  46123  salexct2  46294  aisbnaxb  46860  dandysum2p2e4  46947  iota0ndef  46988  aiota0ndef  47046  257prm  47485  fmtno4nprmfac193  47498  139prmALT  47520  31prm  47521  127prm  47523  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  usgrexmpl2trifr  47931  0nodd  48013  2nodd  48015  1neven  48081  2zrngnring  48101  ex-gt  48958  alsi-no-surprise  49026