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 1106  a4im 1155  ax16 1205  ax16i 1265  wefrc 2933  ordzsl 3106  limuni3 3113  unixp0 3504  funcnvuni 3550  funrnex 3599  tz6.12-2 3724  eqfnfv 3782  oaabs 4236  eceqopreq 4297  php3 4495  pssinf 4507  unbnn2 4522  inf0 4578  inf3lem5 4589  rankxpsuc 4687  aceq5 4712  carduni 4830  cflim 4881  indpi 5006  xrub 6027  fzoptht 6434  basis2t 7557  ubthlem10 8469  ubthlem11 8470  occllem5 9093  atcv0eq 10214  fiiu 10350  fiv 10374  cmphmp 10408  infi 10448  efilcp2 10450  cnfilca 10451

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

Copyright terms: Public domain