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  2850  nemtbir  3024  ru  3739  ruOLD  3740  pssirr  4053  noel  4288  iun0  5010  0iun  5011  br0  5140  vprc  5253  iin0  5300  nfnid  5313  opelopabsb  5470  0nelopab  5505  0nelxp  5650  0xp  5715  nrelv  5740  dm0  5860  cnv0  6087  co02  6208  nlim0  6366  snsn0non  6432  imadif  6565  0fv  6863  poxp2  8073  poseq  8088  tz7.44lem1  8324  nlim1  8404  nlim2  8405  sdom0  9022  canth2  9043  snnen2o  9129  1sdom2  9132  canthp1lem2  10544  pwxpndom2  10556  adderpq  10847  mulerpq  10848  0ncn  11024  ax1ne0  11051  inelr  12115  xrltnr  13018  fzouzdisj  13595  lsw0  14472  eirr  16114  ruc  16152  aleph1re  16154  sqrt2irr  16158  n2dvds1  16279  n2dvds3  16282  sadc0  16365  1nprm  16590  join0  18309  meet0  18310  smndex1n0mnd  18820  nsmndex1  18821  smndex2dnrinv  18823  odhash  19487  cnfldfun  21306  cnfldfunOLD  21319  zringndrg  21406  zfbas  23812  ustn0  24137  zclmncvs  25076  lhop  25949  dvrelog  26574  nosgnn0  27598  sltsolem1  27615  addsrid  27908  muls01  28052  mulsrid  28053  axlowdimlem13  28933  ntrl2v2e  30136  konigsberglem4  30233  avril1  30441  helloworld  30443  topnfbey  30447  vsfval  30611  dmadjrnb  31884  xrge00  32993  esumrnmpt2  34079  measvuni  34225  sibf0  34345  ballotlem4  34510  signswch  34572  satf0n0  35420  fmlaomn0  35432  gonan0  35434  goaln0  35435  fmla0disjsuc  35440  elpotr  35821  dfon2lem7  35829  linedegen  36183  nmotru  36448  limsucncmpi  36485  bj-ru1  36983  bj-0nel1  36993  bj-inftyexpitaudisj  37245  bj-pinftynminfty  37267  finxp0  37431  poimirlem30  37696  coss0  38522  epnsymrel  38605  sn-inelr  42526  diophren  42852  permaxnul  45047  permaxinf2lem  45051  notbicom  45208  rexanuz2nf  45536  stoweidlem44  46088  fourierdlem62  46212  salexct2  46383  aisbnaxb  46948  dandysum2p2e4  47035  iota0ndef  47076  aiota0ndef  47134  257prm  47598  fmtno4nprmfac193  47611  139prmALT  47633  31prm  47634  127prm  47636  nnsum4primeseven  47837  nnsum4primesevenALTV  47838  usgrexmpl2trifr  48074  0nodd  48207  2nodd  48209  1neven  48275  2zrngnring  48295  ex-gt  49766  alsi-no-surprise  49834