Theorem nsyl 116

Description: A negated syllogism inference.

Hypotheses

Ref	Expression
nsyl.1	|- (ph -> -. ps)
nsyl.2	|- (ch -> ps)

Assertion

Ref	Expression
nsyl	|- (ph -> -. ch)

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. 2 |- (ph -> -. ps)
2		nsyl.2	. . 3 |- (ch -> ps)
3	2	con3i 98	. 2 |- (-. ps -> -. ch)
4	1, 3	syl 10	1 |- (ph -> -. ch)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  intnand 691  intnanrd 692  ax6 976  equs4 1146  disjsn 2431  dfwe2 2925  ordnbtwn 3053  funun 3540  tfrlem13 3908  oprssdm 4027  php2 4494  cardaleph 4857  suplem2pr 5134  elnnz 6092  elnnz1 6102  fzneuzt 6450  infpnlem1 7449  filintf 10443

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain