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  1490  fal  1554  eqneltri  2847  nemtbir  3021  ru  3751  ruOLD  3752  pssirr  4066  noel  4301  iun0  5026  0iun  5027  br0  5156  vprc  5270  iin0  5317  nfnid  5330  opelopabsb  5490  0nelopab  5527  0nelxp  5672  0xp  5737  nrelv  5763  dm0  5884  cnv0  6113  co02  6233  nlim0  6392  snsn0non  6459  imadif  6600  0fv  6902  poxp2  8122  poseq  8137  tz7.44lem1  8373  nlim1  8453  nlim2  8454  sdom0  9073  canth2  9094  snnen2o  9184  1sdom2  9187  canthp1lem2  10606  pwxpndom2  10618  adderpq  10909  mulerpq  10910  0ncn  11086  ax1ne0  11113  inelr  12176  xrltnr  13079  fzouzdisj  13656  lsw0  14530  eirr  16173  ruc  16211  aleph1re  16213  sqrt2irr  16217  n2dvds1  16338  n2dvds3  16341  sadc0  16424  1nprm  16649  join0  18364  meet0  18365  smndex1n0mnd  18839  nsmndex1  18840  smndex2dnrinv  18842  odhash  19504  cnfldfun  21278  cnfldfunOLD  21291  zringndrg  21378  zfbas  23783  ustn0  24108  zclmncvs  25048  lhop  25921  dvrelog  26546  nosgnn0  27570  sltsolem1  27587  addsrid  27871  muls01  28015  mulsrid  28016  axlowdimlem13  28881  ntrl2v2e  30087  konigsberglem4  30184  avril1  30392  helloworld  30394  topnfbey  30398  vsfval  30562  dmadjrnb  31835  xrge00  32953  esumrnmpt2  34058  measvuni  34204  sibf0  34325  ballotlem4  34490  signswch  34552  satf0n0  35365  fmlaomn0  35377  gonan0  35379  goaln0  35380  fmla0disjsuc  35385  elpotr  35769  dfon2lem7  35777  linedegen  36131  nmotru  36396  limsucncmpi  36433  bj-ru1  36931  bj-0nel1  36941  bj-inftyexpitaudisj  37193  bj-pinftynminfty  37215  finxp0  37379  poimirlem30  37644  coss0  38470  epnsymrel  38553  sn-inelr  42475  diophren  42801  permaxnul  44998  permaxinf2lem  45002  notbicom  45159  rexanuz2nf  45488  stoweidlem44  46042  fourierdlem62  46166  salexct2  46337  aisbnaxb  46912  dandysum2p2e4  46999  iota0ndef  47040  aiota0ndef  47098  257prm  47562  fmtno4nprmfac193  47575  139prmALT  47597  31prm  47598  127prm  47600  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  usgrexmpl2trifr  48028  0nodd  48158  2nodd  48160  1neven  48226  2zrngnring  48246  ex-gt  49717  alsi-no-surprise  49785