Theorem syl6com 53

Description: Syllogism inference with commuted antecedents.

Hypotheses

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

Assertion

Ref	Expression
syl6com	|- (ps -> (ph -> th))

Proof of Theorem syl6com

Step	Hyp	Ref	Expression
1		syl6com.1	. . 3 |- (ph -> (ps -> ch))
2		syl6com.2	. . 3 |- (ch -> th)
3	1, 2	syl6 22	. 2 |- (ph -> (ps -> th))
4	3	com12 11	1 |- (ps -> (ph -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.61 124  hbimd 1110  a4im 1159  ax16 1209  ax16i 1270  wefrc 2943  ordzsl 3116  limuni3 3123  unixp0 3518  funcnvuni 3564  funrnex 3613  tz6.12-2 3739  eqfnfv 3797  oaabs 4252  eceqopreq 4313  php3 4515  php3OLD 4516  pssinfOLD 4528  unbnn2 4545  inf0 4606  inf3lem5 4617  rankxpsuc 4715  aceq5 4740  carduni 4858  cflim 4909  indpi 5034  xrub 6080  fzoptht 6502  basis2t 7615  ubthlem10 8538  ubthlem11 8539  occllem5 9177  atcv0eq 10306  fiiu 10453  fiiuOLD 10454  fiv 10482  fivOLD 10483  cmphmp 10521  infi 10578  infiOLD 10579  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem6 10595  rcfpfillem6OLD 10596

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

Copyright terms: Public domain