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  5097  nnsuc  7826  poxp2  8085  frrlem14  8241  unxpdomlem2  9157  oismo  9445  cnfcom3lem  9612  rankelb  9736  fin33i  10279  isf34lem4  10287  canthp1lem2  10564  gchdju1  10567  pwfseqlem3  10571  inttsk  10685  r1tskina  10693  nqereu  10840  zbtwnre  12859  discr1  14162  seqcoll2  14388  bitsfzo  16362  bitsf1  16373  eucalglt  16512  4sqlem17  16889  4sqlem18  16890  ramubcl  16946  psgnunilem5  19423  odnncl  19474  gexnnod  19517  sylow1lem1  19527  torsubg  19783  prmcyg  19823  ablfacrplem  19996  pgpfac1lem2  20006  pgpfac1lem3a  20007  pgpfac1lem3  20008  xrsdsreclblem  21367  prmirredlem  21427  ppttop  22951  pptbas  22952  regr1lem  23683  alexsublem  23988  reconnlem1  24771  metnrmlem1a  24803  vitalilem4  25568  vitalilem5  25569  itg2gt0  25717  rollelem  25949  lhop1lem  25974  coefv0  26209  plyexmo  26277  lgamucov  27004  ppinprm  27118  chtnprm  27120  lgsdir  27299  lgseisenlem1  27342  2sqlem7  27391  2sqblem  27398  pntpbnd1  27553  madebdaylemlrcut  27895  bdayfinbndlem1  28463  dfon2lem8  35982  poimirlem25  37842  fdc  37942  ac6s6  38369  2atm  39783  llnmlplnN  39795  trlval3  40443  cdleme0moN  40481  cdleme18c  40549  qirropth  43146  aacllem  50042