Theorem mt3d 150

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 147	. 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  151  nsyl2OLD  152  olcnd  874  ecase23d  1470  disjss3  5029  nnsuc  7577  unxpdomlem2  8707  oismo  8988  cnfcom3lem  9150  rankelb  9237  fin33i  9780  isf34lem4  9788  canthp1lem2  10064  gchdju1  10067  pwfseqlem3  10071  inttsk  10185  r1tskina  10193  nqereu  10340  zbtwnre  12334  discr1  13596  seqcoll2  13819  bitsfzo  15774  bitsf1  15785  eucalglt  15919  4sqlem17  16287  4sqlem18  16288  ramubcl  16344  psgnunilem5  18614  odnncl  18665  gexnnod  18705  sylow1lem1  18715  torsubg  18967  prmcyg  19007  ablfacrplem  19180  pgpfac1lem2  19190  pgpfac1lem3a  19191  pgpfac1lem3  19192  xrsdsreclblem  20137  prmirredlem  20186  ppttop  21612  pptbas  21613  regr1lem  22344  alexsublem  22649  reconnlem1  23431  metnrmlem1a  23463  vitalilem4  24215  vitalilem5  24216  itg2gt0  24364  rollelem  24592  lhop1lem  24616  coefv0  24845  plyexmo  24909  lgamucov  25623  ppinprm  25737  chtnprm  25739  lgsdir  25916  lgseisenlem1  25959  2sqlem7  26008  2sqblem  26015  pntpbnd1  26170  dfon2lem8  33148  frrlem14  33249  poimirlem25  35082  fdc  35183  ac6s6  35610  2atm  36823  llnmlplnN  36835  trlval3  37483  cdleme0moN  37521  cdleme18c  37589  qirropth  39849  aacllem  45329