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  1474  disjss3  5148  nnsuc  7873  poxp2  8129  frrlem14  8284  unxpdomlem2  9251  oismo  9535  cnfcom3lem  9698  rankelb  9819  fin33i  10364  isf34lem4  10372  canthp1lem2  10648  gchdju1  10651  pwfseqlem3  10655  inttsk  10769  r1tskina  10777  nqereu  10924  zbtwnre  12930  discr1  14202  seqcoll2  14426  bitsfzo  16376  bitsf1  16387  eucalglt  16522  4sqlem17  16894  4sqlem18  16895  ramubcl  16951  psgnunilem5  19362  odnncl  19413  gexnnod  19456  sylow1lem1  19466  torsubg  19722  prmcyg  19762  ablfacrplem  19935  pgpfac1lem2  19945  pgpfac1lem3a  19946  pgpfac1lem3  19947  xrsdsreclblem  20991  prmirredlem  21042  ppttop  22510  pptbas  22511  regr1lem  23243  alexsublem  23548  reconnlem1  24342  metnrmlem1a  24374  vitalilem4  25128  vitalilem5  25129  itg2gt0  25278  rollelem  25506  lhop1lem  25530  coefv0  25762  plyexmo  25826  lgamucov  26542  ppinprm  26656  chtnprm  26658  lgsdir  26835  lgseisenlem1  26878  2sqlem7  26927  2sqblem  26934  pntpbnd1  27089  madebdaylemlrcut  27393  dfon2lem8  34762  poimirlem25  36513  fdc  36613  ac6s6  37040  2atm  38398  llnmlplnN  38410  trlval3  39058  cdleme0moN  39096  cdleme18c  39164  qirropth  41646  aacllem  47848