Theorem syl9r 58

Description: A nested syllogism inference with different antecedents.

Hypotheses

Ref	Expression
syl9r.1	|- (ph -> (ps -> ch))
syl9r.2	|- (th -> (ch -> ta))

Assertion

Ref	Expression
syl9r	|- (th -> (ph -> (ps -> ta)))

Proof of Theorem syl9r

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3 |- (ph -> (ps -> ch))
2		syl9r.2	. . 3 |- (th -> (ch -> ta))
3	1, 2	syl9 57	. 2 |- (ph -> (th -> (ps -> ta)))
4	3	com12 11	1 |- (th -> (ph -> (ps -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  sylan9r 469  hbsb4 1248  a16g 1276  oneqmin 3018  fununi 3563  dfimafn 3761  funimass3 3806  isomin 3899  tz7.48lem 3955  sdomen2 4482  trcl 4645  indpi 5034  infxpidmlem7 7558  lmcau 7996  minveclem27 8571  hlimcaui 9106  spansn 9480

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

Copyright terms: Public domain