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 223	. 2 ⊢ (𝜓 ↔ 𝜑)
4	1, 3	mtbi 322	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  2847  nemtbir  3033  ru  3773  pssirr  4096  indifdirOLD  4281  noel  4326  noelOLD  4327  iun0  5059  0iun  5060  br0  5191  vprc  5309  iin0  5356  nfnid  5369  opelopabsb  5526  0nelopab  5563  0nelxp  5706  0xp  5770  nrelv  5796  dm0  5917  cnv0  6139  co02  6258  nlim0  6422  snsn0non  6488  imadif  6631  0fv  6935  poxp2  8140  poseq  8155  tz7.44lem1  8417  nlim1  8501  nlim2  8502  sdom0  9122  canth2  9144  snnen2o  9251  1sdom2  9254  canthp1lem2  10662  pwxpndom2  10674  adderpq  10965  mulerpq  10966  0ncn  11142  ax1ne0  11169  inelr  12218  xrltnr  13117  fzouzdisj  13686  lsw0  14533  eirr  16167  ruc  16205  aleph1re  16207  sqrt2irr  16211  n2dvds1  16330  n2dvds3  16333  sadc0  16414  1nprm  16635  join0  18382  meet0  18383  smndex1n0mnd  18849  nsmndex1  18850  smndex2dnrinv  18852  odhash  19513  cnfldfun  21273  cnfldfunOLD  21286  zringndrg  21374  zfbas  23774  ustn0  24099  zclmncvs  25050  lhop  25923  dvrelog  26545  nosgnn0  27565  sltsolem1  27582  addsrid  27855  muls01  27986  mulsrid  27987  axlowdimlem13  28739  ntrl2v2e  29942  konigsberglem4  30039  avril1  30247  helloworld  30249  topnfbey  30253  vsfval  30417  dmadjrnb  31690  xrge00  32711  esumrnmpt2  33610  measvuni  33756  sibf0  33877  ballotlem4  34041  signswch  34116  satf0n0  34911  fmlaomn0  34923  gonan0  34925  goaln0  34926  fmla0disjsuc  34931  elpotr  35300  dfon2lem7  35308  linedegen  35662  nmotru  35815  limsucncmpi  35852  bj-ru1  36345  bj-0nel1  36355  bj-inftyexpitaudisj  36607  bj-pinftynminfty  36629  finxp0  36793  poimirlem30  37045  coss0  37875  epnsymrel  37958  diophren  42145  notbicom  44450  rexanuz2nf  44788  stoweidlem44  45345  fourierdlem62  45469  salexct2  45640  aisbnaxb  46206  dandysum2p2e4  46293  iota0ndef  46334  aiota0ndef  46390  257prm  46814  fmtno4nprmfac193  46827  139prmALT  46849  31prm  46850  127prm  46852  nnsum4primeseven  47053  nnsum4primesevenALTV  47054  0nodd  47145  2nodd  47147  1neven  47213  2zrngnring  47233  ex-gt  48072  alsi-no-surprise  48142