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  878  disjss3  5085  nnsuc  7828  poxp2  8086  frrlem14  8242  unxpdomlem2  9160  oismo  9448  cnfcom3lem  9615  rankelb  9739  fin33i  10282  isf34lem4  10290  canthp1lem2  10567  gchdju1  10570  pwfseqlem3  10574  inttsk  10688  r1tskina  10696  nqereu  10843  zbtwnre  12887  discr1  14192  seqcoll2  14418  bitsfzo  16395  bitsf1  16406  eucalglt  16545  4sqlem17  16923  4sqlem18  16924  ramubcl  16980  psgnunilem5  19460  odnncl  19511  gexnnod  19554  sylow1lem1  19564  torsubg  19820  prmcyg  19860  ablfacrplem  20033  pgpfac1lem2  20043  pgpfac1lem3a  20044  pgpfac1lem3  20045  xrsdsreclblem  21402  prmirredlem  21462  ppttop  22982  pptbas  22983  regr1lem  23714  alexsublem  24019  reconnlem1  24802  metnrmlem1a  24834  vitalilem4  25588  vitalilem5  25589  itg2gt0  25737  rollelem  25966  lhop1lem  25990  coefv0  26223  plyexmo  26290  lgamucov  27015  ppinprm  27129  chtnprm  27131  lgsdir  27309  lgseisenlem1  27352  2sqlem7  27401  2sqblem  27408  pntpbnd1  27563  madebdaylemlrcut  27905  bdayfinbndlem1  28473  dfon2lem8  35986  poimirlem25  37980  fdc  38080  ac6s6  38507  2atm  39987  llnmlplnN  39999  trlval3  40647  cdleme0moN  40685  cdleme18c  40753  qirropth  43354  aacllem  50288