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  1472  disjss3  5147  nnsuc  7905  poxp2  8167  frrlem14  8323  unxpdomlem2  9285  oismo  9578  cnfcom3lem  9741  rankelb  9862  fin33i  10407  isf34lem4  10415  canthp1lem2  10691  gchdju1  10694  pwfseqlem3  10698  inttsk  10812  r1tskina  10820  nqereu  10967  zbtwnre  12986  discr1  14275  seqcoll2  14501  bitsfzo  16469  bitsf1  16480  eucalglt  16619  4sqlem17  16995  4sqlem18  16996  ramubcl  17052  psgnunilem5  19527  odnncl  19578  gexnnod  19621  sylow1lem1  19631  torsubg  19887  prmcyg  19927  ablfacrplem  20100  pgpfac1lem2  20110  pgpfac1lem3a  20111  pgpfac1lem3  20112  xrsdsreclblem  21448  prmirredlem  21501  ppttop  23030  pptbas  23031  regr1lem  23763  alexsublem  24068  reconnlem1  24862  metnrmlem1a  24894  vitalilem4  25660  vitalilem5  25661  itg2gt0  25810  rollelem  26042  lhop1lem  26067  coefv0  26302  plyexmo  26370  lgamucov  27096  ppinprm  27210  chtnprm  27212  lgsdir  27391  lgseisenlem1  27434  2sqlem7  27483  2sqblem  27490  pntpbnd1  27645  madebdaylemlrcut  27952  dfon2lem8  35772  poimirlem25  37632  fdc  37732  ac6s6  38159  2atm  39510  llnmlplnN  39522  trlval3  40170  cdleme0moN  40208  cdleme18c  40276  qirropth  42896  aacllem  49032