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

Theorem mt3d 142
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 141 . 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  143  nsyl2  144  ecase23d  1583  disjss3  4783  nnsuc  7228  unxpdomlem2  8320  oismo  8600  cnfcom3lem  8763  rankelb  8850  fin33i  9392  isf34lem4  9400  canthp1lem2  9676  gchcda1  9679  pwfseqlem3  9683  inttsk  9797  r1tskina  9805  nqereu  9952  zbtwnre  11988  discr1  13206  seqcoll2  13450  bitsfzo  15364  bitsf1  15375  eucalglt  15505  4sqlem17  15871  4sqlem18  15872  ramubcl  15928  psgnunilem5  18120  odnncl  18170  gexnnod  18209  sylow1lem1  18219  torsubg  18463  prmcyg  18501  ablfacrplem  18671  pgpfac1lem2  18681  pgpfac1lem3a  18682  pgpfac1lem3  18683  xrsdsreclblem  20006  prmirredlem  20055  ppttop  21031  pptbas  21032  regr1lem  21762  alexsublem  22067  reconnlem1  22848  metnrmlem1a  22880  vitalilem4  23598  vitalilem5  23599  itg2gt0  23746  rollelem  23971  lhop1lem  23995  coefv0  24223  plyexmo  24287  lgamucov  24984  ppinprm  25098  chtnprm  25100  lgsdir  25277  lgseisenlem1  25320  2sqlem7  25369  2sqblem  25376  pntpbnd1  25495  dfon2lem8  32025  poimirlem25  33760  fdc  33866  ac6s6  34305  2atm  35328  llnmlplnN  35340  trlval3  35989  cdleme0moN  36027  cdleme18c  36095  qirropth  37992  aacllem  43068
  Copyright terms: Public domain W3C validator