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

Theorem mt3d 138
Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
Hypotheses
Ref Expression
mt3d.1 (𝜑 → ¬ 𝜒)
mt3d.2 (𝜑 → (¬ 𝜓𝜒))
Assertion
Ref Expression
mt3d (𝜑𝜓)

Proof of Theorem mt3d
StepHypRef Expression
1 mt3d.1 . 2 (𝜑 → ¬ 𝜒)
2 mt3d.2 . . 3 (𝜑 → (¬ 𝜓𝜒))
32con1d 137 . 2 (𝜑 → (¬ 𝜒𝜓))
41, 3mpd 15 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt3i  139  nsyl2  140  ecase23d  1427  disjss3  4480  nnsuc  6849  unxpdomlem2  7925  oismo  8203  cnfcom3lem  8358  rankelb  8445  fin33i  8949  isf34lem4  8957  canthp1lem2  9229  gchcda1  9232  pwfseqlem3  9236  inttsk  9350  r1tskina  9358  nqereu  9505  zbtwnre  11527  discr1  12729  seqcoll2  12969  bitsfzo  14866  bitsf1  14877  eucalglt  15010  4sqlem17  15385  4sqlem18  15386  ramubcl  15442  psgnunilem5  17627  odnncl  17686  gexnnod  17732  sylow1lem1  17742  torsubg  17985  prmcyg  18023  ablfacrplem  18192  pgpfac1lem2  18202  pgpfac1lem3a  18203  pgpfac1lem3  18204  xrsdsreclblem  19513  prmirredlem  19564  ppttop  20522  pptbas  20523  regr1lem  21253  alexsublem  21559  reconnlem1  22344  metnrmlem1a  22375  metnrmlem1aOLD  22390  vitalilem4  23062  vitalilem5  23063  itg2gt0  23209  rollelem  23432  lhop1lem  23456  coefv0  23693  plyexmo  23757  lgamucov  24452  ppinprm  24568  chtnprm  24570  lgsdir  24747  lgseisenlem1  24790  2sqlem7  24839  2sqblem  24846  pntpbnd1  24965  dfon2lem8  30782  nobndup  30935  nobnddown  30936  nofulllem5  30941  poimirlem25  32479  fdc  32586  ac6s6  33025  2atm  33706  llnmlplnN  33718  trlval3  34367  cdleme0moN  34405  cdleme18c  34473  qirropth  36366  aacllem  42409
  Copyright terms: Public domain W3C validator