Theorem mt3d 125

Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)

Hypotheses

Ref	Expression
mt3d.1
mt3d.2

Assertion

Ref	Expression
mt3d

Proof of Theorem mt3d

Step	Hyp	Ref	Expression
1		mt3d.1	. 2
2		mt3d.2	. . 3
3	2	con1d 124	. 2
4	1, 3	mpd 15	1

Syntax hints:  -.wn 3  ->wi 4

This theorem is referenced by:  mt3i  126  nsyl2  127  ecase23d  1332  disjss3  4451  nnsuc  6717  unxpdomlem2  7745  oismo  7986  cnfcom3lem  8168  cnfcom3lemOLD  8176  rankelb  8263  fin33i  8770  isf34lem4  8778  canthp1lem2  9052  gchcda1  9055  pwfseqlem3  9059  inttsk  9173  r1tskina  9181  nqereu  9328  zbtwnre  11209  discr1  12302  seqcoll2  12513  dvdseq  14033  bitsfzo  14085  bitsf1  14096  eucalglt  14214  4sqlem17  14479  4sqlem18  14480  ramubcl  14536  psgnunilem5  16519  odnncl  16569  gexnnod  16608  sylow1lem1  16618  torsubg  16860  prmcyg  16896  ablfacrplem  17116  pgpfac1lem2  17126  pgpfac1lem3a  17127  pgpfac1lem3  17128  xrsdsreclblem  18464  prmirredlem  18523  prmirredlemOLD  18526  ppttop  19508  pptbas  19509  regr1lem  20240  alexsublem  20544  reconnlem1  21331  metnrmlem1a  21362  vitalilem4  22020  vitalilem5  22021  itg2gt0  22167  rollelem  22390  lhop1lem  22414  coefv0  22645  plyexmo  22709  ppinprm  23426  chtnprm  23428  lgsdir  23605  lgseisenlem1  23624  2sqlem7  23645  2sqblem  23652  pntpbnd1  23771  lgamucov  28580  dfon2lem8  29222  nobndup  29460  nobnddown  29461  nofulllem5  29466  fdc  30238  ac6s6  30580  qirropth  30844  aacllem  33216  2atm  35251  llnmlplnN  35263  trlval3  35912  cdleme0moN  35950  cdleme18c  36018

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