Theorem sylc 68

Description: A syllogism inference combined with contraction.

Hypotheses

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

Assertion

Ref	Expression
sylc	|- (th -> ch)

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.3	. 2 |- (th -> ps)
2		sylc.2	. . 3 |- (th -> ph)
3		sylc.1	. . 3 |- (ph -> (ps -> ch))
4	2, 3	syl 10	. 2 |- (th -> (ps -> ch))
5	1, 4	mpd 26	1 |- (th -> ch)

Syntax hints:   -> wi 3

This theorem is referenced by:  pm2.65d 136  jc 138  jaod 424  sylanc 471  sbc5g 1954  sbc6g 1955  reuuniss2 2891  rabsnt 2894  tz7.7 2973  ssorduni 2993  suceloni 3062  unielrel 3514  zfrep6 3614  tfrlem13 3923  oprabval3 4030  curry1 4098  th3q 4317  f1oen2g 4394  domnsym 4463  limensuci 4506  unfilem3 4550  supmax 4589  inf3lem7 4619  noinfep 4640  r1val1 4658  imadomg 4806  unidom 4808  ltexpri 5149  prlem936 5155  recexpr 5160  supexpr 5163  lemul12it 5844  lemulge11t 5848  nngt0t 5946  nnaddm1clt 5958  supxrunb1 6089  supxrunb2 6090  nn0ltp1let 6127  nn0ind-raph 6214  quoremOLD 6252  qbtwnre 6278  rpge0t 6287  eliooordt 6388  facavgt 6955  climubi 7153  cvgcmp 7184  cvgcmpub 7185  reccnv 7218  erelem3 7321  efaddlem16 7353  efaddlem25 7362  eftabs 7375  abspef01tlub 7395  absefm1le 7412  sin01bndlem2 7468  cos01bndlem2 7470  sin01gt0 7476  cos01gt0 7477  ruclem33 7542  ruclem35 7544  metcnp 7887  tgioolem 7914  lmnn 7935  nmcn3 8341  nmcnc 8342  ubthlem13 8541  pilem2 8672  pilem3 8673  bcsALT 9046  hhcms 9072  hlimcaui 9106  hhsscms 9150  projlem26 9211  projlem27 9212  pjthlem10 9228  ococint 9297  spanpr 9503  osumlem2 9579  osumlem4 9581  pjorth 9614  adjeqt 9859  nmbdoplb 9949  nmcopexlem3 9953  nmcoplb 9958  nmbdfnlb 9978  nmcfnexlem3 9982  nmcfnlb 9987  nmopco 10028  branmfnt 10038  hstnmoct 10150  mdsl0 10237  atoml 10309  atcvat4 10324  atabs 10328  infi1 10447  infi1OLD 10448  truni1 10499  hmphsyma 10528  hmphtr 10531  homcard 10539  fgsb2 10580  cnvtr 10638  rdmob 10681  cmpassoh 10729  homgrf 10730  cmpmon 10743  idmon 10745  immon 10746

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

Copyright terms: Public domain