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  888  disjss3  5098  nnsuc  7860  poxp2  8118  frrlem14  8275  unxpdomlem2  9197  oismo  9485  cnfcom3lem  9655  rankelb  9779  fin33i  10323  isf34lem4  10331  canthp1lem2  10608  gchdju1  10611  pwfseqlem3  10615  inttsk  10729  r1tskina  10737  nqereu  10884  zbtwnre  12944  discr1  14249  seqcoll2  14475  bitsfzo  16452  bitsf1  16463  eucalglt  16602  4sqlem17  16980  4sqlem18  16981  ramubcl  17037  psgnunilem5  19517  odnncl  19568  gexnnod  19611  sylow1lem1  19621  torsubg  19877  prmcyg  19917  ablfacrplem  20090  pgpfac1lem2  20100  pgpfac1lem3a  20101  pgpfac1lem3  20102  xrsdsreclblem  21445  prmirredlem  21504  ppttop  23047  pptbas  23048  regr1lem  23779  alexsublem  24084  reconnlem1  24867  metnrmlem1a  24899  vitalilem4  25653  vitalilem5  25654  itg2gt0  25802  rollelem  26031  lhop1lem  26055  coefv0  26288  plyexmo  26354  lgamucov  27079  ppinprm  27193  chtnprm  27195  lgsdir  27373  lgseisenlem1  27416  2sqlem7  27465  2sqblem  27472  pntpbnd1  27627  madebdaylemlrcut  27969  bdayfinbndlem1  28537  dfon2lem8  36102  poimirlem25  38108  fdc  38208  ac6s6  38635  2atm  40115  llnmlplnN  40127  trlval3  40775  cdleme0moN  40813  cdleme18c  40881  qirropth  43449  aacllem  50386