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  4612  nnsuc  7029  unxpdomlem2  8109  oismo  8389  cnfcom3lem  8544  rankelb  8631  fin33i  9135  isf34lem4  9143  canthp1lem2  9419  gchcda1  9422  pwfseqlem3  9426  inttsk  9540  r1tskina  9548  nqereu  9695  zbtwnre  11730  discr1  12940  seqcoll2  13187  bitsfzo  15081  bitsf1  15092  eucalglt  15222  4sqlem17  15589  4sqlem18  15590  ramubcl  15646  psgnunilem5  17835  odnncl  17885  gexnnod  17924  sylow1lem1  17934  torsubg  18178  prmcyg  18216  ablfacrplem  18385  pgpfac1lem2  18395  pgpfac1lem3a  18396  pgpfac1lem3  18397  xrsdsreclblem  19711  prmirredlem  19760  ppttop  20721  pptbas  20722  regr1lem  21452  alexsublem  21758  reconnlem1  22537  metnrmlem1a  22569  vitalilem4  23286  vitalilem5  23287  itg2gt0  23433  rollelem  23656  lhop1lem  23680  coefv0  23908  plyexmo  23972  lgamucov  24664  ppinprm  24778  chtnprm  24780  lgsdir  24957  lgseisenlem1  25000  2sqlem7  25049  2sqblem  25056  pntpbnd1  25175  dfon2lem8  31396  nobndup  31563  nobnddown  31564  poimirlem25  33066  fdc  33173  ac6s6  33612  2atm  34293  llnmlplnN  34305  trlval3  34954  cdleme0moN  34992  cdleme18c  35060  qirropth  36953  aacllem  41850
  Copyright terms: Public domain W3C validator