MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtbir Structured version   Visualization version   GIF version

Theorem mtbir 312
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
StepHypRef Expression
1 mtbir.1 . 2 ¬ 𝜓
2 mtbir.2 . . 3 (𝜑𝜓)
32bicomi 213 . 2 (𝜓𝜑)
41, 3mtbi 311 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 195
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 196
This theorem is referenced by:  fal  1482  nemtbir  2877  ru  3401  pssirr  3669  indifdir  3842  noel  3878  npss0OLD  3967  iun0  4507  0iun  4508  br0  4626  vprc  4719  iin0  4760  nfnid  4818  opelopabsb  4900  0nelxp  5057  0nelxpOLD  5058  dm0  5247  co02  5552  nlim0  5686  snsn0non  5749  imadif  5873  0fv  6122  snnex  6840  iprc  6971  tfr2b  7357  tz7.44lem1  7366  tz7.48-3  7404  canth2  7976  pwcdadom  8899  canthp1lem2  9332  pwxpndom2  9344  adderpq  9635  mulerpq  9636  0ncn  9811  ax1ne0  9838  pnfnre  9938  mnfnre  9939  inelr  10860  xrltnr  11793  fzouzdisj  12331  lsw0  13154  fprodn0f  14510  eirr  14721  ruc  14760  aleph1re  14762  sqrt2irr  14766  sadc0  14963  1nprm  15179  3prm  15193  prmrec  15413  meet0  16909  join0  16910  odhash  17761  00lsp  18751  zfbas  21458  ustn0  21782  lhop  23528  dvrelog  24128  axlowdimlem13  25580  uvtx01vtx  25814  avril1  26505  helloworld  26507  topnfbey  26511  vsfval  26666  dmadjrnb  27943  xrge00  28811  esumrnmpt2  29251  measvuni  29398  sibf0  29517  ballotlem4  29681  signswch  29758  bnj521  29853  3pm3.2ni  30643  elpotr  30724  dfon2lem7  30732  poseq  30788  nosgnn0  30849  sltsolem1  30861  linedegen  31214  mont  31372  subsym1  31390  limsucncmpi  31408  bj-ru1  31919  bj-0nel1  31927  bj-pinftynrr  32080  bj-minftynrr  32084  bj-pinftynminfty  32085  finxp0  32198  poimirlem30  32403  diophren  36189  eqneltri  38066  stoweidlem44  38731  fourierdlem62  38855  salexct2  39027  aisbnaxb  39521  dandysum2p2e4  39608  257prm  39806  fmtno4nprmfac193  39819  139prmALT  39844  31prm  39845  127prm  39848  nnsum4primeseven  40011  nnsum4primesevenALTV  40012  ntrl2v2e  41317  konigsberglem4  41417  0nodd  41592  2nodd  41594  1neven  41714  2zrngnring  41734  ex-gt  42221  alsi-no-surprise  42304
  Copyright terms: Public domain W3C validator