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  1491  fal  1556  eqneltri  2856  nemtbir  3029  ru  3740  ruOLD  3741  pssirr  4057  noel  4292  vn0  4299  uni0  4893  iun0  5019  0iun  5020  br0  5149  vprc  5262  iin0  5309  nfnid  5322  opelopabsb  5486  0nelopab  5521  0nelxp  5666  nrelv  5757  dm0  5877  cnv0  6105  cnv0OLD  6106  co02  6227  nlim0  6385  snsn0non  6451  imadif  6584  0fv  6883  poxp2  8095  poseq  8110  tz7.44lem1  8346  nlim1  8426  nlim2  8427  sdom0  9049  canth2  9070  snnen2o  9157  1sdom2  9160  canthp1lem2  10576  pwxpndom2  10588  adderpq  10879  mulerpq  10880  0ncn  11056  ax1ne0  11083  inelr  12147  xrltnr  13045  fzouzdisj  13623  lsw0  14500  eirr  16142  ruc  16180  aleph1re  16182  sqrt2irr  16186  n2dvds1  16307  n2dvds3  16310  sadc0  16393  1nprm  16618  join0  18338  meet0  18339  smndex1n0mnd  18849  nsmndex1  18850  smndex2dnrinv  18852  odhash  19515  cnfldfun  21335  cnfldfunOLD  21348  zringndrg  21435  zfbas  23852  ustn0  24177  zclmncvs  25116  lhop  25989  dvrelog  26614  nosgnn0  27638  ltssolem1  27655  addsrid  27972  muls01  28120  mulsrid  28121  axlowdimlem13  29039  ntrl2v2e  30245  konigsberglem4  30342  avril1  30550  helloworld  30552  topnfbey  30556  vsfval  30720  dmadjrnb  31993  xrge00  33106  domnprodeq0  33369  esumrnmpt2  34245  measvuni  34391  sibf0  34511  ballotlem4  34676  signswch  34738  satf0n0  35591  fmlaomn0  35603  gonan0  35605  goaln0  35606  fmla0disjsuc  35611  elpotr  35992  dfon2lem7  36000  linedegen  36356  nmotru  36621  limsucncmpi  36658  bj-ru1  37188  bj-0nel1  37198  bj-inftyexpitaudisj  37457  bj-pinftynminfty  37479  finxp0  37643  poimirlem30  37898  coss0  38817  epnsymrel  38894  sn-inelr  42854  diophren  43167  permaxnul  45361  permaxinf2lem  45365  notbicom  45521  rexanuz2nf  45847  stoweidlem44  46399  fourierdlem62  46523  salexct2  46694  chnerlem1  47237  aisbnaxb  47268  dandysum2p2e4  47355  iota0ndef  47396  aiota0ndef  47454  257prm  47918  fmtno4nprmfac193  47931  139prmALT  47953  31prm  47954  127prm  47956  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  usgrexmpl2trifr  48394  0nodd  48527  2nodd  48529  1neven  48595  2zrngnring  48615  ex-gt  50084  alsi-no-surprise  50152