Theorem mt2d 137

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 135	. 2 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
4	1, 3	mpd 16	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mt2i  138  nsyl3  139  tz7.44-3  8401  sdomdomtr  9112  domsdomtr  9114  infdif  10214  ackbij1b  10244  isf32lem5  10363  alephreg  10595  cfpwsdom  10597  inar1  10788  tskcard  10794  npomex  11009  recnz  12700  rpnnen1lem5  13035  fznuz  13668  uznfz  13669  seqcoll2  14534  ramub1lem1  17124  chnccat  18720  pgpfac1lem1  20209  lsppratlem6  21345  nconnsubb  23654  iunconnlem  23658  clsconn  23661  xkohaus  23885  reconnlem1  25059  ivthlem2  25686  perfectlem1  27473  lgseisenlem1  27619  ex-natded5.8-2  30902  oddpwdc  34873  fineqvinfep  35659  erdszelem9  35786  relowlpssretop  38126  sucneqond  38127  heiborlem8  38576  lcvntr  39907  ncvr1  40153  llnneat  40395  2atnelpln  40425  lplnneat  40426  lplnnelln  40427  3atnelvolN  40467  lvolneatN  40469  lvolnelln  40470  lvolnelpln  40471  lplncvrlvol  40497  4atexlemntlpq  40949  cdleme0nex  41171  nlimsuc  44289