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

Theorem mt3d 150
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 147 . 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  151  nsyl2OLD  152  olcnd  874  ecase23d  1470  disjss3  5041  nnsuc  7582  unxpdomlem2  8711  oismo  8992  cnfcom3lem  9154  rankelb  9241  fin33i  9780  isf34lem4  9788  canthp1lem2  10064  gchdju1  10067  pwfseqlem3  10071  inttsk  10185  r1tskina  10193  nqereu  10340  zbtwnre  12334  discr1  13596  seqcoll2  13819  bitsfzo  15773  bitsf1  15784  eucalglt  15918  4sqlem17  16286  4sqlem18  16287  ramubcl  16343  psgnunilem5  18613  odnncl  18664  gexnnod  18704  sylow1lem1  18714  torsubg  18965  prmcyg  19005  ablfacrplem  19178  pgpfac1lem2  19188  pgpfac1lem3a  19189  pgpfac1lem3  19190  xrsdsreclblem  20135  prmirredlem  20184  ppttop  21610  pptbas  21611  regr1lem  22342  alexsublem  22647  reconnlem1  23429  metnrmlem1a  23461  vitalilem4  24213  vitalilem5  24214  itg2gt0  24362  rollelem  24590  lhop1lem  24614  coefv0  24843  plyexmo  24907  lgamucov  25621  ppinprm  25735  chtnprm  25737  lgsdir  25914  lgseisenlem1  25957  2sqlem7  26006  2sqblem  26013  pntpbnd1  26168  dfon2lem8  33109  frrlem14  33210  poimirlem25  35040  fdc  35141  ac6s6  35568  2atm  36781  llnmlplnN  36793  trlval3  37441  cdleme0moN  37479  cdleme18c  37547  qirropth  39779  aacllem  45268
  Copyright terms: Public domain W3C validator