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

Theorem mt3 171
Description: A rule similar to modus tollens. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mt3.1  |-  -.  ps
mt3.2  |-  ( -. 
ph  ->  ps )
Assertion
Ref Expression
mt3  |-  ph

Proof of Theorem mt3
StepHypRef Expression
1 mt3.1 . . 3  |-  -.  ps
2 mt3.2 . . 3  |-  ( -. 
ph  ->  ps )
31, 2mto 167 . 2  |-  -.  -.  ph
43notnotri 106 1  |-  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  equid  1662  sp  1728  spimeh  1734  cbv3hv  1749  ax9  1902  equidq  2127  sinhalfpilem  19850  wfrlem16  24342  cbv3hvNEW7  29423  ax9NEW7  29445  ax9lem1  29762  ax9lem3  29764  ax9lem12  29773  ax9lem13  29774  ax9vax9  29780
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator