Theorem mtbir 326

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3pm3.2ni  1519  fal  1584  eqneltri  2883  nemtbir  3055  ru  3741  pssirrOLD  4034  noel  4286  noelOLD  4287  vn0  4294  vn0OLD  4295  uni0  4899  iun0  5023  0iun  5024  br0  5158  vprcOLD  5280  iin0  5329  nfnid  5342  opelopabsb  5509  0nelopab  5545  0nelxp  5690  nrelvOLD  5784  cnv0  5869  cnv0OLD  5870  dm0  5910  co02  6278  nlim0  6444  snsn0non  6510  imadif  6649  0fv  6952  poxp2  8190  poseq  8205  tz7.44lem1  8444  nlim1  8528  nlim2  8529  sdom0  9159  canth2  9180  snnen2o  9267  1sdom2  9270  canthp1lem2  10768  pwxpndom2  10780  adderpq  11071  mulerpq  11072  0ncn  11248  ax1ne0  11275  inelr  12340  xrltnr  13278  fzouzdisj  13860  lsw0  14740  eirr  16405  ruc  16443  aleph1re  16445  sqrt2irr  16449  n2dvds1  16570  n2dvds3  16573  sadc0  16656  1nprm  16886  join0  18609  meet0  18610  smndex1n0mnd  19143  nsmndex1  19144  smndex2dnrinv  19146  degenmgmnfn  19168  degenmgm2nfun  19171  odhash  19821  cnfldfun  21725  zringndrg  21807  zfbas  24248  ustn0  24573  zclmncvs  25502  lhop  26369  dvrelog  26998  nosgnn0  28048  ltssolem1  28065  addsrid  28383  muls01  28531  mulsrid  28532  axlowdimlem13  29565  ntrl2v2e  30792  konigsberglem4  30889  avril1  31097  helloworld  31099  topnfbey  31103  nowisdomv  31108  vsfval  31268  dmadjrnb  32541  xrge00  33651  domnprodeq0  33916  esumrnmpt2  34783  measvuni  34930  sibf0  35049  ballotlem4  35214  signswch  35273  satf0n0  36323  fmlaomn0  36335  gonan0  36337  goaln0  36338  fmla0disjsuc  36343  elpotr  36734  dfon2lem7  36742  linedegen  37099  nmotru  37387  limsucncmpi  37424  mh-inf3sn  37521  bj-ru1  38047  bj-0nel1  38057  bj-inftyexpitaudisj  38331  bj-pinftynminfty  38353  finxp0  38519  poimirlem30  38773  coss0  39704  epnsymrel  39781  sn-inelr  43755  diophren  44024  permaxnul  46204  permaxinf2lem  46208  notbicom  46395  rexanuz2nf  46717  stoweidlem44  47269  fourierdlem62  47393  salexct2  47564  chnerlem1  48107  aisbnaxb  48196  dandysum2p2e4  48283  iota0ndef  48324  aiota0ndef  48382  257prm  48861  fmtno4nprmfac193  48874  139prmALT  48896  31prm  48897  127prm  48899  nnsum4primeseven  49113  nnsum4primesevenALTV  49114  usgrexmpl2trifr  49350  0nodd  49482  2nodd  49484  1neven  49550  2zrngnring  49570  ex-gt  51111  als-no-surprise  51214  rals-no-surprise  51215