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  5113  nnsuc  7889  poxp2  8148  frrlem14  8305  unxpdomlem2  9227  oismo  9512  cnfcom3lem  9682  rankelb  9806  fin33i  10371  isf34lem4  10379  canthp1lem2  10656  gchdju1  10659  pwfseqlem3  10663  inttsk  10777  r1tskina  10785  nqereu  10932  zbtwnre  12988  discr1  14295  seqcoll2  14522  bitsfzo  16518  bitsf1  16529  eucalglt  16668  4sqlem17  17046  4sqlem18  17047  ramubcl  17103  psgnunilem5  19595  odnncl  19646  gexnnod  19689  sylow1lem1  19699  torsubg  19955  prmcyg  19995  ablfacrplem  20168  pgpfac1lem2  20178  pgpfac1lem3a  20179  pgpfac1lem3  20180  xrsdsreclblem  21600  prmirredlem  21659  ppttop  23201  pptbas  23202  regr1lem  23933  alexsublem  24238  reconnlem1  25021  metnrmlem1a  25053  vitalilem4  25807  vitalilem5  25808  itg2gt0  25956  rollelem  26185  lhop1lem  26209  coefv0  26442  plyexmo  26511  lgamucov  27239  ppinprm  27353  chtnprm  27355  lgsdir  27533  lgseisenlem1  27576  2sqlem7  27625  2sqblem  27632  pntpbnd1  27787  madebdaylemlrcut  28129  bdayfinbndlem1  28697  dfon2lem8  36301  poimirlem25  38337  fdc  38437  ac6s6  38862  2atm  40342  llnmlplnN  40354  trlval3  41002  cdleme0moN  41040  cdleme18c  41108  qirropth  43676  aacllem  50662