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  3775  pssirr  4099  indifdirOLD  4284  noel  4329  noelOLD  4330  iun0  5064  0iun  5065  br0  5196  vprc  5314  iin0  5359  nfnid  5372  opelopabsb  5529  0nelopab  5566  0nelxp  5709  0xp  5772  nrelv  5798  dm0  5918  cnv0  6137  co02  6256  nlim0  6420  snsn0non  6486  imadif  6629  0fv  6932  poxp2  8124  poseq  8139  tz7.44lem1  8400  nlim1  8484  nlim2  8485  sdom0  9104  canth2  9126  snnen2o  9233  1sdom2  9236  canthp1lem2  10644  pwxpndom2  10656  adderpq  10947  mulerpq  10948  0ncn  11124  ax1ne0  11151  inelr  12198  xrltnr  13095  fzouzdisj  13664  lsw0  14511  eirr  16144  ruc  16182  aleph1re  16184  sqrt2irr  16188  n2dvds1  16307  n2dvds3  16310  sadc0  16391  1nprm  16612  join0  18354  meet0  18355  smndex1n0mnd  18789  nsmndex1  18790  smndex2dnrinv  18792  odhash  19435  cnfldfun  20941  zringndrg  21022  zfbas  23382  ustn0  23707  zclmncvs  24647  lhop  25515  dvrelog  26127  nosgnn0  27141  sltsolem1  27158  addsrid  27428  muls01  27548  mulsrid  27549  axlowdimlem13  28192  ntrl2v2e  29391  konigsberglem4  29488  avril1  29696  helloworld  29698  topnfbey  29702  vsfval  29864  dmadjrnb  31137  xrge00  32165  esumrnmpt2  33004  measvuni  33150  sibf0  33271  ballotlem4  33435  signswch  33510  satf0n0  34307  fmlaomn0  34319  gonan0  34321  goaln0  34322  fmla0disjsuc  34327  elpotr  34691  dfon2lem7  34699  linedegen  35053  nmotru  35231  limsucncmpi  35268  bj-ru1  35762  bj-0nel1  35772  bj-inftyexpitaudisj  36024  bj-pinftynminfty  36046  finxp0  36210  poimirlem30  36456  coss0  37287  epnsymrel  37370  diophren  41484  notbicom  43793  rexanuz2nf  44138  stoweidlem44  44695  fourierdlem62  44819  salexct2  44990  aisbnaxb  45556  dandysum2p2e4  45643  iota0ndef  45684  aiota0ndef  45740  257prm  46164  fmtno4nprmfac193  46177  139prmALT  46199  31prm  46200  127prm  46202  nnsum4primeseven  46403  nnsum4primesevenALTV  46404  0nodd  46515  2nodd  46517  1neven  46732  2zrngnring  46752  ex-gt  47675  alsi-no-surprise  47745