Theorem mt3d 143

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 142	. 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  144  nsyl2  145  ecase23d  1601  disjss3  4874  nnsuc  7348  unxpdomlem2  8440  oismo  8721  cnfcom3lem  8884  rankelb  8971  fin33i  9513  isf34lem4  9521  canthp1lem2  9797  gchcda1  9800  pwfseqlem3  9804  inttsk  9918  r1tskina  9926  nqereu  10073  zbtwnre  12076  discr1  13301  seqcoll2  13545  bitsfzo  15537  bitsf1  15548  eucalglt  15678  4sqlem17  16043  4sqlem18  16044  ramubcl  16100  psgnunilem5  18271  psgnunilem5OLD  18272  odnncl  18322  gexnnod  18361  sylow1lem1  18371  torsubg  18617  prmcyg  18655  ablfacrplem  18825  pgpfac1lem2  18835  pgpfac1lem3a  18836  pgpfac1lem3  18837  xrsdsreclblem  20159  prmirredlem  20208  ppttop  21189  pptbas  21190  regr1lem  21920  alexsublem  22225  reconnlem1  23006  metnrmlem1a  23038  vitalilem4  23784  vitalilem5  23785  itg2gt0  23933  rollelem  24158  lhop1lem  24182  coefv0  24410  plyexmo  24474  lgamucov  25184  ppinprm  25298  chtnprm  25300  lgsdir  25477  lgseisenlem1  25520  2sqlem7  25569  2sqblem  25576  pntpbnd1  25695  dfon2lem8  32228  poimirlem25  33973  fdc  34078  ac6s6  34516  2atm  35597  llnmlplnN  35609  trlval3  36257  cdleme0moN  36295  cdleme18c  36363  qirropth  38311  aacllem  43453