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

Theorem mt3d 125
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 124 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
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:  mt3i  126  nsyl2  127  ecase23d  1322  disjss3  4286  nnsuc  6488  unxpdomlem2  7510  oismo  7746  cnfcom3lem  7928  cnfcom3lemOLD  7936  rankelb  8023  fin33i  8530  isf34lem4  8538  canthp1lem2  8812  gchcda1  8815  pwfseqlem3  8819  inttsk  8933  r1tskina  8941  nqereu  9090  zbtwnre  10943  discr1  11992  seqcoll2  12209  dvdseq  13572  bitsfzo  13623  bitsf1  13634  eucalglt  13752  4sqlem17  14014  4sqlem18  14015  ramubcl  14071  psgnunilem5  15991  odnncl  16039  gexnnod  16078  sylow1lem1  16088  torsubg  16327  prmcyg  16361  ablfacrplem  16556  pgpfac1lem2  16566  pgpfac1lem3a  16567  pgpfac1lem3  16568  xrsdsreclblem  17839  prmirredlem  17897  prmirredlemOLD  17900  ppttop  18591  pptbas  18592  regr1lem  19292  alexsublem  19596  reconnlem1  20383  metnrmlem1a  20414  vitalilem4  21071  vitalilem5  21072  itg2gt0  21218  rollelem  21441  lhop1lem  21465  coefv0  21695  plyexmo  21759  ppinprm  22470  chtnprm  22472  lgsdir  22649  lgseisenlem1  22668  2sqlem7  22689  2sqblem  22696  pntpbnd1  22815  lgamucov  26993  dfon2lem8  27572  nobndup  27810  nobnddown  27811  nofulllem5  27816  fdc  28612  ac6s6  28955  qirropth  29220  2atm  33064  llnmlplnN  33076  trlval3  33724  cdleme0moN  33762  cdleme18c  33830
  Copyright terms: Public domain W3C validator