Theorem mt2d 136

Description: Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)

Hypotheses

Ref	Expression
mt2d.1	⊢ (𝜑 → 𝜒)
mt2d.2	⊢ (𝜑 → (𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
mt2d	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mt2d

Step	Hyp	Ref	Expression
1		mt2d.1	. 2 ⊢ (𝜑 → 𝜒)
2		mt2d.2	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	2	con2d 134	. 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:  mt2i  137  nsyl3  138  tz7.44-3  8340  sdomdomtr  9041  domsdomtr  9043  infdif  10121  ackbij1b  10151  isf32lem5  10270  alephreg  10496  cfpwsdom  10498  inar1  10689  tskcard  10695  npomex  10910  recnz  12595  rpnnen1lem5  12922  fznuz  13554  uznfz  13555  seqcoll2  14418  ramub1lem1  16988  chnccat  18583  pgpfac1lem1  20042  lsppratlem6  21142  nconnsubb  23398  iunconnlem  23402  clsconn  23405  xkohaus  23628  reconnlem1  24802  ivthlem2  25429  perfectlem1  27206  lgseisenlem1  27352  ex-natded5.8-2  30499  oddpwdc  34514  fineqvinfep  35285  erdszelem9  35397  relowlpssretop  37694  sucneqond  37695  heiborlem8  38153  lcvntr  39486  ncvr1  39732  llnneat  39974  2atnelpln  40004  lplnneat  40005  lplnnelln  40006  3atnelvolN  40046  lvolneatN  40048  lvolnelln  40049  lvolnelpln  40050  lplncvrlvol  40076  4atexlemntlpq  40528  cdleme0nex  40750  nlimsuc  43886