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 214 . 2 (𝜓𝜑)
41, 3mtbi 311 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  fal  1639  nemtbir  3027  ru  3575  pssirr  3849  indifdir  4026  noel  4062  npss0OLD  4158  iun0  4728  0iun  4729  br0  4853  vprc  4948  iin0  4988  nfnid  5046  opelopabsb  5135  0nelxp  5300  0nelxpOLD  5301  0xp  5356  nrelv  5400  dm0  5494  cnv0  5693  co02  5810  nlim0  5944  snsn0non  6007  imadif  6134  0fv  6388  snnexOLD  7132  iprc  7266  tfr2b  7661  tz7.44lem1  7670  tz7.48-3  7708  canth2  8278  pwcdadom  9230  canthp1lem2  9667  pwxpndom2  9679  adderpq  9970  mulerpq  9971  0ncn  10146  ax1ne0  10173  pnfnre  10273  mnfnre  10274  inelr  11202  xrltnr  12146  fzouzdisj  12698  lsw0  13539  fprodn0f  14921  eirr  15132  ruc  15171  aleph1re  15173  sqrt2irr  15178  sadc0  15378  1nprm  15594  3prm  15608  prmrec  15828  meet0  17338  join0  17339  odhash  18189  00lsp  19183  cnfldfunALT  19961  zringndrg  20040  zfbas  21901  ustn0  22225  zclmncvs  23148  lhop  23978  dvrelog  24582  axlowdimlem13  26033  ntrl2v2e  27310  konigsberglem4  27407  avril1  27630  helloworld  27632  topnfbey  27636  vsfval  27797  dmadjrnb  29074  xrge00  29995  esumrnmpt2  30439  measvuni  30586  sibf0  30705  ballotlem4  30869  signswch  30947  bnj521  31112  3pm3.2ni  31901  elpotr  31991  dfon2lem7  31999  poseq  32059  nosgnn0  32117  sltsolem1  32132  linedegen  32556  mont  32714  subsym1  32732  limsucncmpi  32750  bj-ru1  33239  bj-0nel1  33246  bj-pinftynrr  33420  bj-minftynrr  33424  bj-pinftynminfty  33425  finxp0  33539  poimirlem30  33752  coss0  34552  epnsymrel  34631  diophren  37879  eqneltri  39745  stoweidlem44  40764  fourierdlem62  40888  salexct2  41060  aisbnaxb  41584  dandysum2p2e4  41671  257prm  41983  fmtno4nprmfac193  41996  139prmALT  42021  31prm  42022  127prm  42025  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  0nodd  42320  2nodd  42322  1neven  42442  2zrngnring  42462  ex-gt  42982  alsi-no-surprise  43055
  Copyright terms: Public domain W3C validator