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  1555  eqneltri  2848  nemtbir  3022  ru  3737  ruOLD  3738  pssirr  4051  noel  4286  iun0  5008  0iun  5009  br0  5138  vprc  5251  iin0  5298  nfnid  5311  opelopabsb  5468  0nelopab  5503  0nelxp  5648  0xp  5713  nrelv  5738  dm0  5858  cnv0  6084  co02  6204  nlim0  6362  snsn0non  6428  imadif  6561  0fv  6858  poxp2  8068  poseq  8083  tz7.44lem1  8319  nlim1  8399  nlim2  8400  sdom0  9017  canth2  9038  snnen2o  9124  1sdom2  9127  canthp1lem2  10536  pwxpndom2  10548  adderpq  10839  mulerpq  10840  0ncn  11016  ax1ne0  11043  inelr  12107  xrltnr  13010  fzouzdisj  13587  lsw0  14464  eirr  16106  ruc  16144  aleph1re  16146  sqrt2irr  16150  n2dvds1  16271  n2dvds3  16274  sadc0  16357  1nprm  16582  join0  18301  meet0  18302  smndex1n0mnd  18812  nsmndex1  18813  smndex2dnrinv  18815  odhash  19479  cnfldfun  21298  cnfldfunOLD  21311  zringndrg  21398  zfbas  23804  ustn0  24129  zclmncvs  25068  lhop  25941  dvrelog  26566  nosgnn0  27590  sltsolem1  27607  addsrid  27900  muls01  28044  mulsrid  28045  axlowdimlem13  28925  ntrl2v2e  30128  konigsberglem4  30225  avril1  30433  helloworld  30435  topnfbey  30439  vsfval  30603  dmadjrnb  31876  xrge00  32985  esumrnmpt2  34071  measvuni  34217  sibf0  34337  ballotlem4  34502  signswch  34564  satf0n0  35390  fmlaomn0  35402  gonan0  35404  goaln0  35405  fmla0disjsuc  35410  elpotr  35794  dfon2lem7  35802  linedegen  36156  nmotru  36421  limsucncmpi  36458  bj-ru1  36956  bj-0nel1  36966  bj-inftyexpitaudisj  37218  bj-pinftynminfty  37240  finxp0  37404  poimirlem30  37669  coss0  38495  epnsymrel  38578  sn-inelr  42499  diophren  42825  permaxnul  45020  permaxinf2lem  45024  notbicom  45181  rexanuz2nf  45509  stoweidlem44  46061  fourierdlem62  46185  salexct2  46356  aisbnaxb  46921  dandysum2p2e4  47008  iota0ndef  47049  aiota0ndef  47107  257prm  47571  fmtno4nprmfac193  47584  139prmALT  47606  31prm  47607  127prm  47609  nnsum4primeseven  47810  nnsum4primesevenALTV  47811  usgrexmpl2trifr  48047  0nodd  48180  2nodd  48182  1neven  48248  2zrngnring  48268  ex-gt  49739  alsi-no-surprise  49807