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  4576  nnsuc  6951  unxpdomlem2  8027  oismo  8305  cnfcom3lem  8460  rankelb  8547  fin33i  9051  isf34lem4  9059  canthp1lem2  9331  gchcda1  9334  pwfseqlem3  9338  inttsk  9452  r1tskina  9460  nqereu  9607  zbtwnre  11618  discr1  12817  seqcoll2  13058  bitsfzo  14941  bitsf1  14952  eucalglt  15082  4sqlem17  15449  4sqlem18  15450  ramubcl  15506  psgnunilem5  17683  odnncl  17733  gexnnod  17772  sylow1lem1  17782  torsubg  18026  prmcyg  18064  ablfacrplem  18233  pgpfac1lem2  18243  pgpfac1lem3a  18244  pgpfac1lem3  18245  xrsdsreclblem  19557  prmirredlem  19605  ppttop  20563  pptbas  20564  regr1lem  21294  alexsublem  21600  reconnlem1  22369  metnrmlem1a  22400  vitalilem4  23103  vitalilem5  23104  itg2gt0  23250  rollelem  23473  lhop1lem  23497  coefv0  23725  plyexmo  23789  lgamucov  24481  ppinprm  24595  chtnprm  24597  lgsdir  24774  lgseisenlem1  24817  2sqlem7  24866  2sqblem  24873  pntpbnd1  24992  dfon2lem8  30745  nobndup  30905  nobnddown  30906  nofulllem5  30911  poimirlem25  32407  fdc  32514  ac6s6  32953  2atm  33634  llnmlplnN  33646  trlval3  34295  cdleme0moN  34333  cdleme18c  34401  qirropth  36294  aacllem  42319
  Copyright terms: Public domain W3C validator