Theorem mt3d 139

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 138	. 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  140  nsyl2  141  ecase23d  1428  disjss3  4582  nnsuc  6974  unxpdomlem2  8050  oismo  8328  cnfcom3lem  8483  rankelb  8570  fin33i  9074  isf34lem4  9082  canthp1lem2  9354  gchcda1  9357  pwfseqlem3  9361  inttsk  9475  r1tskina  9483  nqereu  9630  zbtwnre  11662  discr1  12862  seqcoll2  13106  bitsfzo  14995  bitsf1  15006  eucalglt  15136  4sqlem17  15503  4sqlem18  15504  ramubcl  15560  psgnunilem5  17737  odnncl  17787  gexnnod  17826  sylow1lem1  17836  torsubg  18080  prmcyg  18118  ablfacrplem  18287  pgpfac1lem2  18297  pgpfac1lem3a  18298  pgpfac1lem3  18299  xrsdsreclblem  19611  prmirredlem  19660  ppttop  20621  pptbas  20622  regr1lem  21352  alexsublem  21658  reconnlem1  22437  metnrmlem1a  22469  vitalilem4  23186  vitalilem5  23187  itg2gt0  23333  rollelem  23556  lhop1lem  23580  coefv0  23808  plyexmo  23872  lgamucov  24564  ppinprm  24678  chtnprm  24680  lgsdir  24857  lgseisenlem1  24900  2sqlem7  24949  2sqblem  24956  pntpbnd1  25075  dfon2lem8  30939  nobndup  31099  nobnddown  31100  nofulllem5  31105  poimirlem25  32604  fdc  32711  ac6s6  33150  2atm  33831  llnmlplnN  33843  trlval3  34492  cdleme0moN  34530  cdleme18c  34598  qirropth  36491  aacllem  42356