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 ⊢ (𝜑 → 𝜓)

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  150  olcnd  890  disjss3  5104  nnsuc  7868  poxp2  8127  frrlem14  8284  unxpdomlem2  9205  oismo  9490  cnfcom3lem  9660  rankelb  9784  fin33i  10341  isf34lem4  10349  canthp1lem2  10626  gchdju1  10629  pwfseqlem3  10633  inttsk  10747  r1tskina  10755  nqereu  10902  zbtwnre  12961  discr1  14266  seqcoll2  14492  bitsfzo  16483  bitsf1  16494  eucalglt  16633  4sqlem17  17011  4sqlem18  17012  ramubcl  17068  psgnunilem5  19555  odnncl  19606  gexnnod  19649  sylow1lem1  19659  torsubg  19915  prmcyg  19955  ablfacrplem  20128  pgpfac1lem2  20138  pgpfac1lem3a  20139  pgpfac1lem3  20140  xrsdsreclblem  21523  prmirredlem  21582  ppttop  23125  pptbas  23126  regr1lem  23857  alexsublem  24162  reconnlem1  24945  metnrmlem1a  24977  vitalilem4  25731  vitalilem5  25732  itg2gt0  25880  rollelem  26109  lhop1lem  26133  coefv0  26366  plyexmo  26435  lgamucov  27160  ppinprm  27274  chtnprm  27276  lgsdir  27454  lgseisenlem1  27497  2sqlem7  27546  2sqblem  27553  pntpbnd1  27708  madebdaylemlrcut  28050  bdayfinbndlem1  28618  dfon2lem8  36151  poimirlem25  38156  fdc  38256  ac6s6  38683  2atm  40163  llnmlplnN  40175  trlval3  40823  cdleme0moN  40861  cdleme18c  40929  qirropth  43497  aacllem  50430