Metamath Proof Explorer

Theorem nsyl5

Description: A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024)

Ref Expression
Hypotheses nsyl4.1 
|- ( ph -> ps )
nsyl4.2 
|- ( -. ph -> ch )
Assertion nsyl5 
|- ( -. ps -> ch )

Proof

Step Hyp Ref Expression
1 nsyl4.1 
 |-  ( ph -> ps )
2 nsyl4.2 
 |-  ( -. ph -> ch )
3 1 2 nsyl4 
 |-  ( -. ch -> ps )
4 3 con1i 
 |-  ( -. ps -> ch )