HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem mtod 108
Description: Modus tollens deduction.
Hypotheses
Ref Expression
mtod.1 |- (ph -> -. ch)
mtod.2 |- (ph -> (ps -> ch))
Assertion
Ref Expression
mtod |- (ph -> -. ps)
Proof of Theorem mtod
StepHypRef Expression
1 mtod.1 . 2 |- (ph -> -. ch)
2 mtod.2 . . 3 |- (ph -> (ps -> ch))
32con3d 95 . 2 |- (ph -> (-. ch -> -. ps))
41, 3mpd 26 1 |- (ph -> -. ps)
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3
This theorem is referenced by:  mtbid 712  mtbird 713  po2nr 2838  po3nr 2839  ordn2lp 2958  onsucuni2 3081  onssneli 3091  nlimsucg 3102  tfi 3116  nnlim 3134  peano5 3143  tz7.48-3 3943  oalimcl 4178  omlimcl 4193  oneo 4196  sdomnsym 4442  php3 4495  onomeneq 4498  rankr1 4646  rankel 4652  ondomcard 4829  alephordi 4846  cardaleph 4857  ltrpq 5057  prlem934 5111  suplem2pr 5134  zneo 6147  zneoOLD 6148  sqr2irrlem3 6656  abssubne0t 6820  facndivt 6880  climrecl 7047  ivthlem6 7221  ivthlem6OLD 7230  lmle 7895  nvex 8169  efif1lem5 8649  irredlem1 10225
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
Copyright terms: Public domain