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

Theorem mtbir 324
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 225 . 2 (𝜓𝜑)
41, 3mtbi 323 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207
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 208
This theorem is referenced by:  fal  1542  eqneltri  2903  nemtbir  3109  ru  3768  pssirr  4074  indifdir  4257  noel  4293  noelOLD  4294  iun0  4976  0iun  4977  br0  5106  vprc  5210  iin0  5252  nfnid  5267  opelopabsb  5408  0nelxp  5582  0xp  5642  nrelv  5666  dm0  5783  cnv0  5992  co02  6106  nlim0  6242  snsn0non  6302  imadif  6431  0fv  6702  tz7.44lem1  8030  canth2  8658  canthp1lem2  10063  pwxpndom2  10075  adderpq  10366  mulerpq  10367  0ncn  10543  ax1ne0  10570  inelr  11616  xrltnr  12502  fzouzdisj  13061  lsw0  13905  eirr  15546  ruc  15584  aleph1re  15586  sqrt2irr  15590  n2dvds1  15705  n2dvds3  15709  sadc0  15791  1nprm  16011  meet0  17735  join0  17736  odhash  18628  cnfldfunALT  20486  zringndrg  20565  zfbas  22432  ustn0  22756  zclmncvs  23679  lhop  24540  dvrelog  25147  axlowdimlem13  26667  ntrl2v2e  27864  konigsberglem4  27961  avril1  28169  helloworld  28171  topnfbey  28175  vsfval  28337  dmadjrnb  29610  xrge00  30600  esumrnmpt2  31226  measvuni  31372  sibf0  31491  ballotlem4  31655  signswch  31730  bnj521  31906  satf0n0  32522  fmlaomn0  32534  gonan0  32536  goaln0  32537  fmla0disjsuc  32542  3pm3.2ni  32840  elpotr  32923  dfon2lem7  32931  poseq  32992  nosgnn0  33062  sltsolem1  33077  linedegen  33501  nmotru  33653  subsym1  33672  limsucncmpi  33690  bj-ru1  34151  bj-0nel1  34162  bj-inftyexpitaudisj  34379  bj-pinftynminfty  34401  bj-isrvec  34463  finxp0  34554  poimirlem30  34803  coss0  35599  epnsymrel  35678  diophren  39288  stoweidlem44  42206  fourierdlem62  42330  salexct2  42499  aisbnaxb  43024  dandysum2p2e4  43111  iota0ndef  43151  aiota0ndef  43172  257prm  43600  fmtno4nprmfac193  43613  139prmALT  43636  31prm  43637  127prm  43640  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  0nodd  43954  2nodd  43956  smndex1n0mnd  44012  nsmndex1  44013  smndex2dnrinv  44015  1neven  44131  2zrngnring  44151  ex-gt  44755  alsi-no-surprise  44825
  Copyright terms: Public domain W3C validator