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  ecase23d  1474  disjss3  5141  nnsuc  7906  poxp2  8169  frrlem14  8325  unxpdomlem2  9288  oismo  9581  cnfcom3lem  9744  rankelb  9865  fin33i  10410  isf34lem4  10418  canthp1lem2  10694  gchdju1  10697  pwfseqlem3  10701  inttsk  10815  r1tskina  10823  nqereu  10970  zbtwnre  12989  discr1  14279  seqcoll2  14505  bitsfzo  16473  bitsf1  16484  eucalglt  16623  4sqlem17  17000  4sqlem18  17001  ramubcl  17057  psgnunilem5  19513  odnncl  19564  gexnnod  19607  sylow1lem1  19617  torsubg  19873  prmcyg  19913  ablfacrplem  20086  pgpfac1lem2  20096  pgpfac1lem3a  20097  pgpfac1lem3  20098  xrsdsreclblem  21431  prmirredlem  21484  ppttop  23015  pptbas  23016  regr1lem  23748  alexsublem  24053  reconnlem1  24849  metnrmlem1a  24881  vitalilem4  25647  vitalilem5  25648  itg2gt0  25796  rollelem  26028  lhop1lem  26053  coefv0  26288  plyexmo  26356  lgamucov  27082  ppinprm  27196  chtnprm  27198  lgsdir  27377  lgseisenlem1  27420  2sqlem7  27469  2sqblem  27476  pntpbnd1  27631  madebdaylemlrcut  27938  dfon2lem8  35792  poimirlem25  37653  fdc  37753  ac6s6  38180  2atm  39530  llnmlplnN  39542  trlval3  40190  cdleme0moN  40228  cdleme18c  40296  qirropth  42924  aacllem  49375