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  disjss3  5090  nnsuc  7814  poxp2  8073  frrlem14  8229  unxpdomlem2  9141  oismo  9426  cnfcom3lem  9593  rankelb  9714  fin33i  10257  isf34lem4  10265  canthp1lem2  10541  gchdju1  10544  pwfseqlem3  10548  inttsk  10662  r1tskina  10670  nqereu  10817  zbtwnre  12841  discr1  14143  seqcoll2  14369  bitsfzo  16343  bitsf1  16354  eucalglt  16493  4sqlem17  16870  4sqlem18  16871  ramubcl  16927  psgnunilem5  19404  odnncl  19455  gexnnod  19498  sylow1lem1  19508  torsubg  19764  prmcyg  19804  ablfacrplem  19977  pgpfac1lem2  19987  pgpfac1lem3a  19988  pgpfac1lem3  19989  xrsdsreclblem  21347  prmirredlem  21407  ppttop  22920  pptbas  22921  regr1lem  23652  alexsublem  23957  reconnlem1  24740  metnrmlem1a  24772  vitalilem4  25537  vitalilem5  25538  itg2gt0  25686  rollelem  25918  lhop1lem  25943  coefv0  26178  plyexmo  26246  lgamucov  26973  ppinprm  27087  chtnprm  27089  lgsdir  27268  lgseisenlem1  27311  2sqlem7  27360  2sqblem  27367  pntpbnd1  27522  madebdaylemlrcut  27842  dfon2lem8  35823  poimirlem25  37684  fdc  37784  ac6s6  38211  2atm  39565  llnmlplnN  39577  trlval3  40225  cdleme0moN  40263  cdleme18c  40331  qirropth  42940  aacllem  49832