Theorem mtbir 325

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

Syntax hints:  ¬ wn 3   ↔ wb 208

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 209

This theorem is referenced by:  3pm3.2ni  1508  fal  1573  eqneltri  2880  nemtbir  3052  ru  3741  pssirrOLD  4055  noel  4288  vn0  4295  uni0  4891  iun0  5016  0iun  5017  br0  5146  vprcOLD  5268  iin0  5316  nfnid  5329  opelopabsb  5497  0nelopab  5532  0nelxp  5677  nrelvOLD  5769  cnv0  5851  cnv0OLD  5852  dm0  5892  co02  6242  nlim0  6400  snsn0non  6466  imadif  6599  0fv  6902  poxp2  8116  poseq  8131  tz7.44lem1  8369  nlim1  8451  nlim2  8452  sdom0  9074  canth2  9095  snnen2o  9182  1sdom2  9185  canthp1lem2  10604  pwxpndom2  10616  adderpq  10907  mulerpq  10908  0ncn  11084  ax1ne0  11111  inelr  12178  xrltnr  13114  fzouzdisj  13694  lsw0  14571  eirr  16227  ruc  16265  aleph1re  16267  sqrt2irr  16271  n2dvds1  16392  n2dvds3  16395  sadc0  16478  1nprm  16703  join0  18425  meet0  18426  smndex1n0mnd  18939  nsmndex1  18940  smndex2dnrinv  18942  odhash  19604  cnfldfun  21425  zringndrg  21507  zfbas  23943  ustn0  24268  zclmncvs  25197  lhop  26065  dvrelog  26689  nosgnn0  27709  ltssolem1  27726  addsrid  28044  muls01  28192  mulsrid  28193  axlowdimlem13  29111  ntrl2v2e  30316  konigsberglem4  30413  avril1  30621  helloworld  30623  topnfbey  30627  nowisdomv  30632  vsfval  30792  dmadjrnb  32065  xrge00  33152  domnprodeq0  33420  esumrnmpt2  34325  measvuni  34471  sibf0  34591  ballotlem4  34756  signswch  34815  satf0n0  35688  fmlaomn0  35700  gonan0  35702  goaln0  35703  fmla0disjsuc  35708  elpotr  36089  dfon2lem7  36097  linedegen  36453  nmotru  36728  limsucncmpi  36765  mh-inf3sn  36862  bj-ru1  37388  bj-0nel1  37398  bj-inftyexpitaudisj  37657  bj-pinftynminfty  37679  finxp0  37845  poimirlem30  38109  coss0  39028  epnsymrel  39105  sn-inelr  43069  diophren  43350  permaxnul  45544  permaxinf2lem  45548  notbicom  45703  rexanuz2nf  46026  stoweidlem44  46578  fourierdlem62  46702  salexct2  46873  chnerlem1  47418  aisbnaxb  47465  dandysum2p2e4  47552  iota0ndef  47593  aiota0ndef  47651  257prm  48130  fmtno4nprmfac193  48143  139prmALT  48165  31prm  48166  127prm  48168  nnsum4primeseven  48382  nnsum4primesevenALTV  48383  usgrexmpl2trifr  48619  0nodd  48752  2nodd  48754  1neven  48820  2zrngnring  48840  ex-gt  50309  alsi-no-surprise  50377