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  5147  nnsuc  7870  poxp2  8126  frrlem14  8281  unxpdomlem2  9248  oismo  9532  cnfcom3lem  9695  rankelb  9816  fin33i  10361  isf34lem4  10369  canthp1lem2  10645  gchdju1  10648  pwfseqlem3  10652  inttsk  10766  r1tskina  10774  nqereu  10921  zbtwnre  12927  discr1  14199  seqcoll2  14423  bitsfzo  16373  bitsf1  16384  eucalglt  16519  4sqlem17  16891  4sqlem18  16892  ramubcl  16948  psgnunilem5  19357  odnncl  19408  gexnnod  19451  sylow1lem1  19461  torsubg  19717  prmcyg  19757  ablfacrplem  19930  pgpfac1lem2  19940  pgpfac1lem3a  19941  pgpfac1lem3  19942  xrsdsreclblem  20984  prmirredlem  21034  ppttop  22502  pptbas  22503  regr1lem  23235  alexsublem  23540  reconnlem1  24334  metnrmlem1a  24366  vitalilem4  25120  vitalilem5  25121  itg2gt0  25270  rollelem  25498  lhop1lem  25522  coefv0  25754  plyexmo  25818  lgamucov  26532  ppinprm  26646  chtnprm  26648  lgsdir  26825  lgseisenlem1  26868  2sqlem7  26917  2sqblem  26924  pntpbnd1  27079  madebdaylemlrcut  27383  dfon2lem8  34751  poimirlem25  36502  fdc  36602  ac6s6  37029  2atm  38387  llnmlplnN  38399  trlval3  39047  cdleme0moN  39085  cdleme18c  39153  qirropth  41632  aacllem  47802