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 1243  a16g 1271  oneqmin 3008  fununi 3549  dfimafn 3746  funimass3 3791  isomin 3884  tz7.48lem 3940  sdomen2 4462  trcl 4617  indpi 5006  infxpidmlem7 7501  lmcau 7930  minveclem27 8502  hlimcaui 9027  spansn 9396

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

Copyright terms: Public domain