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  8337  sdomdomtr  9034  domsdomtr  9036  infdif  10121  ackbij1b  10151  isf32lem5  10270  alephreg  10495  cfpwsdom  10497  inar1  10688  tskcard  10694  npomex  10909  recnz  12569  rpnnen1lem5  12900  fznuz  13530  uznfz  13531  seqcoll2  14390  ramub1lem1  16956  pgpfac1lem1  19973  lsppratlem6  21077  nconnsubb  23326  iunconnlem  23330  clsconn  23333  xkohaus  23556  reconnlem1  24731  ivthlem2  25369  perfectlem1  27156  lgseisenlem1  27302  ex-natded5.8-2  30376  oddpwdc  34321  erdszelem9  35171  relowlpssretop  37337  sucneqond  37338  heiborlem8  37797  lcvntr  39004  ncvr1  39250  llnneat  39493  2atnelpln  39523  lplnneat  39524  lplnnelln  39525  3atnelvolN  39565  lvolneatN  39567  lvolnelln  39568  lvolnelpln  39569  lplncvrlvol  39595  4atexlemntlpq  40047  cdleme0nex  40269  nlimsuc  43414