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

Theorem mt3d 140
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 139 . 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  141  nsyl2  142  ecase23d  1433  disjss3  4622  nnsuc  7044  unxpdomlem2  8125  oismo  8405  cnfcom3lem  8560  rankelb  8647  fin33i  9151  isf34lem4  9159  canthp1lem2  9435  gchcda1  9438  pwfseqlem3  9442  inttsk  9556  r1tskina  9564  nqereu  9711  zbtwnre  11746  discr1  12956  seqcoll2  13203  bitsfzo  15100  bitsf1  15111  eucalglt  15241  4sqlem17  15608  4sqlem18  15609  ramubcl  15665  psgnunilem5  17854  odnncl  17904  gexnnod  17943  sylow1lem1  17953  torsubg  18197  prmcyg  18235  ablfacrplem  18404  pgpfac1lem2  18414  pgpfac1lem3a  18415  pgpfac1lem3  18416  xrsdsreclblem  19732  prmirredlem  19781  ppttop  20751  pptbas  20752  regr1lem  21482  alexsublem  21788  reconnlem1  22569  metnrmlem1a  22601  vitalilem4  23320  vitalilem5  23321  itg2gt0  23467  rollelem  23690  lhop1lem  23714  coefv0  23942  plyexmo  24006  lgamucov  24698  ppinprm  24812  chtnprm  24814  lgsdir  24991  lgseisenlem1  25034  2sqlem7  25083  2sqblem  25090  pntpbnd1  25209  dfon2lem8  31449  nobndup  31616  nobnddown  31617  poimirlem25  33105  fdc  33212  ac6s6  33651  2atm  34332  llnmlplnN  34344  trlval3  34993  cdleme0moN  35031  cdleme18c  35099  qirropth  36992  aacllem  41880
  Copyright terms: Public domain W3C validator