Theorem mt3d 149

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 146	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
4	1, 3	mpd 16	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt3i  150  olcnd  891  disjss3  5101  nnsuc  7895  poxp2  8162  frrlem14  8320  unxpdomlem2  9251  oismo  9537  cnfcom3lem  9707  rankelb  9836  fin33i  10450  isf34lem4  10458  canthp1lem2  10741  gchdju1  10744  pwfseqlem3  10748  inttsk  10862  r1tskina  10870  nqereu  11017  zbtwnre  13076  discr1  14386  seqcoll2  14613  bitsfzo  16610  bitsf1  16621  eucalglt  16765  4sqlem17  17144  4sqlem18  17145  ramubcl  17201  psgnunilem5  19713  odnncl  19764  gexnnod  19807  sylow1lem1  19817  torsubg  20073  prmcyg  20113  ablfacrplem  20286  pgpfac1lem2  20296  pgpfac1lem3a  20297  pgpfac1lem3  20298  xrsdsreclblem  21724  prmirredlem  21783  ppttop  23330  pptbas  23331  regr1lem  24063  alexsublem  24368  reconnlem1  25151  metnrmlem1a  25183  vitalilem4  25937  vitalilem5  25938  itg2gt0  26086  rollelem  26314  lhop1lem  26338  coefv0  26572  plyexmo  26641  lgamucov  27370  chtnprm  27486  lgsdir  27664  lgseisenlem1  27707  2sqlem7  27756  2sqblem  27763  pntpbnd1  27918  madebdaylemlrcut  28290  bdayfinbndlem1  28858  dfon2lem8  36644  poimirlem25  38656  fdc  38772  ac6s6  39197  2atm  40677  llnmlplnN  40689  trlval3  41337  cdleme0moN  41375  cdleme18c  41443  qirropth  44008  aacllem  51107