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  5105  nnsuc  7919  poxp2  8187  frrlem14  8345  unxpdomlem2  9276  oismo  9561  cnfcom3lem  9731  rankelb  9860  fin33i  10474  isf34lem4  10482  canthp1lem2  10765  gchdju1  10768  pwfseqlem3  10772  inttsk  10886  r1tskina  10894  nqereu  11041  zbtwnre  13100  discr1  14410  seqcoll2  14637  bitsfzo  16634  bitsf1  16645  eucalglt  16789  4sqlem17  17168  4sqlem18  17169  ramubcl  17225  psgnunilem5  19738  odnncl  19789  gexnnod  19832  sylow1lem1  19842  torsubg  20098  prmcyg  20138  ablfacrplem  20311  pgpfac1lem2  20321  pgpfac1lem3a  20322  pgpfac1lem3  20323  xrsdsreclblem  21749  prmirredlem  21808  ppttop  23355  pptbas  23356  regr1lem  24088  alexsublem  24393  reconnlem1  25176  metnrmlem1a  25208  vitalilem4  25962  vitalilem5  25963  itg2gt0  26111  rollelem  26339  lhop1lem  26363  coefv0  26597  plyexmo  26666  lgamucov  27395  chtnprm  27511  lgsdir  27689  lgseisenlem1  27732  2sqlem7  27781  2sqblem  27788  pntpbnd1  27943  madebdaylemlrcut  28315  bdayfinbndlem1  28883  dfon2lem8  36730  poimirlem25  38755  fdc  38871  ac6s6  39296  2atm  40776  llnmlplnN  40788  trlval3  41436  cdleme0moN  41474  cdleme18c  41542  qirropth  44108  aacllem  51219