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  876  ecase23d  1473  disjss3  5165  nnsuc  7921  poxp2  8184  frrlem14  8340  unxpdomlem2  9314  oismo  9609  cnfcom3lem  9772  rankelb  9893  fin33i  10438  isf34lem4  10446  canthp1lem2  10722  gchdju1  10725  pwfseqlem3  10729  inttsk  10843  r1tskina  10851  nqereu  10998  zbtwnre  13011  discr1  14288  seqcoll2  14514  bitsfzo  16481  bitsf1  16492  eucalglt  16632  4sqlem17  17008  4sqlem18  17009  ramubcl  17065  psgnunilem5  19536  odnncl  19587  gexnnod  19630  sylow1lem1  19640  torsubg  19896  prmcyg  19936  ablfacrplem  20109  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  xrsdsreclblem  21453  prmirredlem  21506  ppttop  23035  pptbas  23036  regr1lem  23768  alexsublem  24073  reconnlem1  24867  metnrmlem1a  24899  vitalilem4  25665  vitalilem5  25666  itg2gt0  25815  rollelem  26047  lhop1lem  26072  coefv0  26307  plyexmo  26373  lgamucov  27099  ppinprm  27213  chtnprm  27215  lgsdir  27394  lgseisenlem1  27437  2sqlem7  27486  2sqblem  27493  pntpbnd1  27648  madebdaylemlrcut  27955  dfon2lem8  35754  poimirlem25  37605  fdc  37705  ac6s6  38132  2atm  39484  llnmlplnN  39496  trlval3  40144  cdleme0moN  40182  cdleme18c  40250  qirropth  42864  aacllem  48895