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

Step	Hyp	Ref	Expression
1		mt3d.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mt3d.2	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
3	2	con1d 139	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜓)

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  1436  disjss3  4652  nnsuc  7082  unxpdomlem2  8165  oismo  8445  cnfcom3lem  8600  rankelb  8687  fin33i  9191  isf34lem4  9199  canthp1lem2  9475  gchcda1  9478  pwfseqlem3  9482  inttsk  9596  r1tskina  9604  nqereu  9751  zbtwnre  11786  discr1  13000  seqcoll2  13249  bitsfzo  15157  bitsf1  15168  eucalglt  15298  4sqlem17  15665  4sqlem18  15666  ramubcl  15722  psgnunilem5  17914  odnncl  17964  gexnnod  18003  sylow1lem1  18013  torsubg  18257  prmcyg  18295  ablfacrplem  18464  pgpfac1lem2  18474  pgpfac1lem3a  18475  pgpfac1lem3  18476  xrsdsreclblem  19792  prmirredlem  19841  ppttop  20811  pptbas  20812  regr1lem  21542  alexsublem  21848  reconnlem1  22629  metnrmlem1a  22661  vitalilem4  23380  vitalilem5  23381  itg2gt0  23527  rollelem  23752  lhop1lem  23776  coefv0  24004  plyexmo  24068  lgamucov  24764  ppinprm  24878  chtnprm  24880  lgsdir  25057  lgseisenlem1  25100  2sqlem7  25149  2sqblem  25156  pntpbnd1  25275  dfon2lem8  31695  poimirlem25  33434  fdc  33541  ac6s6  33980  2atm  34813  llnmlplnN  34825  trlval3  35474  cdleme0moN  35512  cdleme18c  35580  qirropth  37473  aacllem  42547