MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mt3d Unicode version

Theorem mt3d 119
Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
Hypotheses
Ref Expression
mt3d.1  |-  ( ph  ->  -.  ch )
mt3d.2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Assertion
Ref Expression
mt3d  |-  ( ph  ->  ps )

Proof of Theorem mt3d
StepHypRef Expression
1 mt3d.1 . 2  |-  ( ph  ->  -.  ch )
2 mt3d.2 . . 3  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32con1d 118 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mpd 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt3i  120  nsyl2  121  ecase23d  1290  disjss3  3982  nnsuc  4631  unxpdomlem2  7022  oismo  7209  cnfcom3lem  7360  rankelb  7450  fin33i  7949  isf34lem4  7957  canthp1lem2  8229  gchcda1  8232  pwfseqlem3  8236  inttsk  8350  r1tskina  8358  nqereu  8507  zbtwnre  10267  discr1  11189  seqcoll2  11353  dvdseq  12524  bitsfzo  12574  bitsf1  12585  eucalglt  12703  4sqlem17  12956  4sqlem18  12957  ramubcl  13013  odnncl  14808  gexnnod  14847  sylow1lem1  14857  torsubg  15094  prmcyg  15128  ablfacrplem  15248  pgpfac1lem2  15258  pgpfac1lem3a  15259  pgpfac1lem3  15260  xrsdsreclblem  16365  prmirredlem  16394  ppttop  16692  pptbas  16693  regr1lem  17378  alexsublem  17686  reconnlem1  18279  metnrmlem1a  18310  vitalilem4  18914  vitalilem5  18915  itg2gt0  19063  rollelem  19284  lhop1lem  19308  coefv0  19577  plyexmo  19641  ppinprm  20338  chtnprm  20340  lgsdir  20517  lgseisenlem1  20536  2sqlem7  20557  2sqblem  20564  pntpbnd1  20683  dfon2lem8  23501  axfelem9  23709  axfelem10  23710  axfelem18  23718  fdc  25808  qirropth  26346  psgnunilem5  26770  2atm  28867  llnmlplnN  28879  trlval3  29527  cdleme0moN  29565  cdleme18c  29633
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator