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  1489  fal  1556  eqneltri  2853  nemtbir  3039  ru  3776  pssirr  4100  indifdirOLD  4285  noel  4330  noelOLD  4331  iun0  5065  0iun  5066  br0  5197  vprc  5315  iin0  5360  nfnid  5373  opelopabsb  5530  0nelopab  5567  0nelxp  5710  0xp  5773  nrelv  5799  dm0  5919  cnv0  6138  co02  6257  nlim0  6421  snsn0non  6487  imadif  6630  0fv  6933  poxp2  8126  poseq  8141  tz7.44lem1  8402  nlim1  8486  nlim2  8487  sdom0  9105  canth2  9127  snnen2o  9234  1sdom2  9237  canthp1lem2  10645  pwxpndom2  10657  adderpq  10948  mulerpq  10949  0ncn  11125  ax1ne0  11152  inelr  12199  xrltnr  13096  fzouzdisj  13665  lsw0  14512  eirr  16145  ruc  16183  aleph1re  16185  sqrt2irr  16189  n2dvds1  16308  n2dvds3  16311  sadc0  16392  1nprm  16613  join0  18355  meet0  18356  smndex1n0mnd  18790  nsmndex1  18791  smndex2dnrinv  18793  odhash  19437  cnfldfun  20949  zringndrg  21030  zfbas  23392  ustn0  23717  zclmncvs  24657  lhop  25525  dvrelog  26137  nosgnn0  27151  sltsolem1  27168  addsrid  27438  muls01  27558  mulsrid  27559  axlowdimlem13  28202  ntrl2v2e  29401  konigsberglem4  29498  avril1  29706  helloworld  29708  topnfbey  29712  vsfval  29874  dmadjrnb  31147  xrge00  32175  esumrnmpt2  33055  measvuni  33201  sibf0  33322  ballotlem4  33486  signswch  33561  satf0n0  34358  fmlaomn0  34370  gonan0  34372  goaln0  34373  fmla0disjsuc  34378  elpotr  34742  dfon2lem7  34750  linedegen  35104  nmotru  35282  limsucncmpi  35319  bj-ru1  35813  bj-0nel1  35823  bj-inftyexpitaudisj  36075  bj-pinftynminfty  36097  finxp0  36261  poimirlem30  36507  coss0  37338  epnsymrel  37421  diophren  41537  notbicom  43846  rexanuz2nf  44190  stoweidlem44  44747  fourierdlem62  44871  salexct2  45042  aisbnaxb  45608  dandysum2p2e4  45695  iota0ndef  45736  aiota0ndef  45792  257prm  46216  fmtno4nprmfac193  46229  139prmALT  46251  31prm  46252  127prm  46254  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  0nodd  46567  2nodd  46569  1neven  46784  2zrngnring  46804  ex-gt  47727  alsi-no-surprise  47797