Theorem mt2d 117

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 115	. 2
4	1, 3	mpd 15	1

Syntax hints:  -.wn 3  ->wi 4

This theorem is referenced by:  mt2i  118  nsyl3  119  tz7.44-3  7093  sdomdomtr  7670  domsdomtr  7672  infdif  8610  ackbij1b  8640  isf32lem5  8758  alephreg  8978  cfpwsdom  8980  inar1  9174  tskcard  9180  npomex  9395  recnz  10963  rpnnen1lem5  11241  fznuz  11789  uznfz  11790  seqcoll2  12513  ramub1lem1  14544  pgpfac1lem1  17125  lsppratlem6  17798  nconsubb  19924  iunconlem  19928  clscon  19931  xkohaus  20154  reconnlem1  21331  ivthlem2  21864  perfectlem1  23504  lgseisenlem1  23624  ex-natded5.8-2  25135  oddpwdc  28293  erdszelem9  28643  heiborlem8  30314  lcvntr  34751  ncvr1  34997  llnneat  35238  2atnelpln  35268  lplnneat  35269  lplnnelln  35270  3atnelvolN  35310  lvolneatN  35312  lvolnelln  35313  lvolnelpln  35314  lplncvrlvol  35340  4atexlemntlpq  35792  cdleme0nex  36015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8