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  1644  sp  1716  spimeh  1722  cbv3hv  1737  ax9  1889  equidq  2114  sinhalfpilem  19834  wfrlem16  24271  ax9lem1  29140  ax9lem3  29142  ax9lem12  29151  ax9lem13  29152  ax9vax9  29158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator