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  874  ecase23d  1472  disjss3  5073  nnsuc  7730  frrlem14  8115  unxpdomlem2  9028  oismo  9299  cnfcom3lem  9461  rankelb  9582  fin33i  10125  isf34lem4  10133  canthp1lem2  10409  gchdju1  10412  pwfseqlem3  10416  inttsk  10530  r1tskina  10538  nqereu  10685  zbtwnre  12686  discr1  13954  seqcoll2  14179  bitsfzo  16142  bitsf1  16153  eucalglt  16290  4sqlem17  16662  4sqlem18  16663  ramubcl  16719  psgnunilem5  19102  odnncl  19153  gexnnod  19193  sylow1lem1  19203  torsubg  19455  prmcyg  19495  ablfacrplem  19668  pgpfac1lem2  19678  pgpfac1lem3a  19679  pgpfac1lem3  19680  xrsdsreclblem  20644  prmirredlem  20694  ppttop  22157  pptbas  22158  regr1lem  22890  alexsublem  23195  reconnlem1  23989  metnrmlem1a  24021  vitalilem4  24775  vitalilem5  24776  itg2gt0  24925  rollelem  25153  lhop1lem  25177  coefv0  25409  plyexmo  25473  lgamucov  26187  ppinprm  26301  chtnprm  26303  lgsdir  26480  lgseisenlem1  26523  2sqlem7  26572  2sqblem  26579  pntpbnd1  26734  dfon2lem8  33766  poxp2  33790  poxp3  33796  madebdaylemlrcut  34079  poimirlem25  35802  fdc  35903  ac6s6  36330  2atm  37541  llnmlplnN  37553  trlval3  38201  cdleme0moN  38239  cdleme18c  38307  qirropth  40730  aacllem  46505