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  5106  nnsuc  7884  poxp2  8145  frrlem14  8302  unxpdomlem2  9231  oismo  9516  cnfcom3lem  9686  rankelb  9810  fin33i  10375  isf34lem4  10383  canthp1lem2  10666  gchdju1  10669  pwfseqlem3  10673  inttsk  10787  r1tskina  10795  nqereu  10942  zbtwnre  12999  discr1  14307  seqcoll2  14534  bitsfzo  16531  bitsf1  16542  eucalglt  16681  4sqlem17  17059  4sqlem18  17060  ramubcl  17116  psgnunilem5  19627  odnncl  19678  gexnnod  19721  sylow1lem1  19731  torsubg  19987  prmcyg  20027  ablfacrplem  20200  pgpfac1lem2  20210  pgpfac1lem3a  20211  pgpfac1lem3  20212  xrsdsreclblem  21632  prmirredlem  21691  ppttop  23238  pptbas  23239  regr1lem  23971  alexsublem  24276  reconnlem1  25059  metnrmlem1a  25091  vitalilem4  25845  vitalilem5  25846  itg2gt0  25994  rollelem  26223  lhop1lem  26247  coefv0  26481  plyexmo  26552  lgamucov  27282  chtnprm  27398  lgsdir  27576  lgseisenlem1  27619  2sqlem7  27668  2sqblem  27675  pntpbnd1  27830  madebdaylemlrcut  28172  bdayfinbndlem1  28740  dfon2lem8  36375  poimirlem25  38402  fdc  38503  ac6s6  38928  2atm  40408  llnmlplnN  40420  trlval3  41068  cdleme0moN  41106  cdleme18c  41174  qirropth  43757  aacllem  50780