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  8210  sdomdomtr  8846  domsdomtr  8848  infdif  9896  ackbij1b  9926  isf32lem5  10044  alephreg  10269  cfpwsdom  10271  inar1  10462  tskcard  10468  npomex  10683  recnz  12325  rpnnen1lem5  12650  fznuz  13267  uznfz  13268  seqcoll2  14107  ramub1lem1  16655  pgpfac1lem1  19592  lsppratlem6  20329  nconnsubb  22482  iunconnlem  22486  clsconn  22489  xkohaus  22712  reconnlem1  23895  ivthlem2  24521  perfectlem1  26282  lgseisenlem1  26428  ex-natded5.8-2  28679  oddpwdc  32221  erdszelem9  33061  relowlpssretop  35462  sucneqond  35463  heiborlem8  35903  lcvntr  36967  ncvr1  37213  llnneat  37455  2atnelpln  37485  lplnneat  37486  lplnnelln  37487  3atnelvolN  37527  lvolneatN  37529  lvolnelln  37530  lvolnelpln  37531  lplncvrlvol  37557  4atexlemntlpq  38009  cdleme0nex  38231