Theorem mt2d 130

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 128	. 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  131  nsyl3  132  tz7.44-3  7391  sdomdomtr  7978  domsdomtr  7980  infdif  8914  ackbij1b  8944  isf32lem5  9062  alephreg  9283  cfpwsdom  9285  inar1  9476  tskcard  9482  npomex  9697  recnz  11328  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  fznuz  12291  uznfz  12292  seqcoll2  13106  ramub1lem1  15568  pgpfac1lem1  18296  lsppratlem6  18973  nconsubb  21036  iunconlem  21040  clscon  21043  xkohaus  21266  reconnlem1  22437  ivthlem2  23028  perfectlem1  24754  lgseisenlem1  24900  ex-natded5.8-2  26663  oddpwdc  29743  erdszelem9  30435  relowlpssretop  32388  sucneqond  32389  heiborlem8  32787  lcvntr  33331  ncvr1  33577  llnneat  33818  2atnelpln  33848  lplnneat  33849  lplnnelln  33850  3atnelvolN  33890  lvolneatN  33892  lvolnelln  33893  lvolnelpln  33894  lplncvrlvol  33920  4atexlemntlpq  34372  cdleme0nex  34595