Theorem mt2d 131

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

Hypotheses

Ref	Expression
mt2d.1	|- ( ph -> ch )
mt2d.2	|- ( ph -> ( ps -> -. ch ) )

Assertion

Ref	Expression
mt2d	|- ( ph -> -. ps )

Proof of Theorem mt2d

Step	Hyp	Ref	Expression
1		mt2d.1	. 2 |- ( ph -> ch )
2		mt2d.2	. . 3 |- ( ph -> ( ps -> -. ch ) )
3	2	con2d 129	. 2 |- ( ph -> ( ch -> -. ps ) )
4	1, 3	mpd 15	1 |- ( ph -> -. ps )

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  132  nsyl3  133  tz7.44-3  7504  sdomdomtr  8093  domsdomtr  8095  infdif  9031  ackbij1b  9061  isf32lem5  9179  alephreg  9404  cfpwsdom  9406  inar1  9597  tskcard  9603  npomex  9818  recnz  11452  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  fznuz  12422  uznfz  12423  seqcoll2  13249  ramub1lem1  15730  pgpfac1lem1  18473  lsppratlem6  19152  nconnsubb  21226  iunconnlem  21230  clsconn  21233  xkohaus  21456  reconnlem1  22629  ivthlem2  23221  perfectlem1  24954  lgseisenlem1  25100  ex-natded5.8-2  27271  oddpwdc  30416  erdszelem9  31181  relowlpssretop  33212  sucneqond  33213  heiborlem8  33617  lcvntr  34313  ncvr1  34559  llnneat  34800  2atnelpln  34830  lplnneat  34831  lplnnelln  34832  3atnelvolN  34872  lvolneatN  34874  lvolnelln  34875  lvolnelpln  34876  lplncvrlvol  34902  4atexlemntlpq  35354  cdleme0nex  35577