Theorem mt3d 142

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 141	. 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  143  nsyl2  144  ecase23d  1584  disjss3  4785  nnsuc  7229  unxpdomlem2  8321  oismo  8601  cnfcom3lem  8764  rankelb  8851  fin33i  9393  isf34lem4  9401  canthp1lem2  9677  gchcda1  9680  pwfseqlem3  9684  inttsk  9798  r1tskina  9806  nqereu  9953  zbtwnre  11989  discr1  13207  seqcoll2  13451  bitsfzo  15365  bitsf1  15376  eucalglt  15506  4sqlem17  15872  4sqlem18  15873  ramubcl  15929  psgnunilem5  18121  odnncl  18171  gexnnod  18210  sylow1lem1  18220  torsubg  18464  prmcyg  18502  ablfacrplem  18672  pgpfac1lem2  18682  pgpfac1lem3a  18683  pgpfac1lem3  18684  xrsdsreclblem  20007  prmirredlem  20056  ppttop  21032  pptbas  21033  regr1lem  21763  alexsublem  22068  reconnlem1  22849  metnrmlem1a  22881  vitalilem4  23599  vitalilem5  23600  itg2gt0  23747  rollelem  23972  lhop1lem  23996  coefv0  24224  plyexmo  24288  lgamucov  24985  ppinprm  25099  chtnprm  25101  lgsdir  25278  lgseisenlem1  25321  2sqlem7  25370  2sqblem  25377  pntpbnd1  25496  dfon2lem8  32031  poimirlem25  33767  fdc  33873  ac6s6  34312  2atm  35335  llnmlplnN  35347  trlval3  35996  cdleme0moN  36034  cdleme18c  36102  qirropth  37999  aacllem  43078