Theorem mt3d 148

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 145	. 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  149  olcnd  877  disjss3  5106  nnsuc  7860  poxp2  8122  frrlem14  8278  unxpdomlem2  9198  oismo  9493  cnfcom3lem  9656  rankelb  9777  fin33i  10322  isf34lem4  10330  canthp1lem2  10606  gchdju1  10609  pwfseqlem3  10613  inttsk  10727  r1tskina  10735  nqereu  10882  zbtwnre  12905  discr1  14204  seqcoll2  14430  bitsfzo  16405  bitsf1  16416  eucalglt  16555  4sqlem17  16932  4sqlem18  16933  ramubcl  16989  psgnunilem5  19424  odnncl  19475  gexnnod  19518  sylow1lem1  19528  torsubg  19784  prmcyg  19824  ablfacrplem  19997  pgpfac1lem2  20007  pgpfac1lem3a  20008  pgpfac1lem3  20009  xrsdsreclblem  21329  prmirredlem  21382  ppttop  22894  pptbas  22895  regr1lem  23626  alexsublem  23931  reconnlem1  24715  metnrmlem1a  24747  vitalilem4  25512  vitalilem5  25513  itg2gt0  25661  rollelem  25893  lhop1lem  25918  coefv0  26153  plyexmo  26221  lgamucov  26948  ppinprm  27062  chtnprm  27064  lgsdir  27243  lgseisenlem1  27286  2sqlem7  27335  2sqblem  27342  pntpbnd1  27497  madebdaylemlrcut  27810  dfon2lem8  35778  poimirlem25  37639  fdc  37739  ac6s6  38166  2atm  39521  llnmlplnN  39533  trlval3  40181  cdleme0moN  40219  cdleme18c  40287  qirropth  42896  aacllem  49790