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 1950  sbc6g 1951  reuuniss2 2886  rabsnt 2889  tz7.7 2968  ssorduni 2988  suceloni 3057  unielrel 3506  zfrep6 3606  tfrlem13 3914  oprabval3 4021  curry1 4088  th3q 4307  f1oen2g 4381  domnsym 4449  limensuci 4492  unfilem3 4532  supmax 4569  inf3lem7 4599  noinfep 4620  r1val1 4638  imadomg 4786  unidom 4788  ltexpri 5129  prlem936 5135  recexpr 5140  supexpr 5143  lemul12it 5808  nngt0t 5902  nnaddm1clt 5913  supxrunb1 6044  supxrunb2 6045  nn0ltp1let 6082  nn0ind-raph 6170  qbtwnre 6224  rpge0t 6233  ioossicc 6338  facavgt 6900  climubi 7097  cvgcmp 7128  cvgcmpub 7129  reccnv 7161  erelem3 7271  efaddlem16 7303  efaddlem25 7312  eftabs 7325  abspef01tlub 7344  absefm1le 7360  sin01bndlem2 7418  cos01bndlem2 7420  sin01gt0 7426  cos01gt0 7427  ruclem33 7493  ruclem35 7495  metcnp 7839  tgioolem 7866  lmnn 7887  nmcnc 8289  ubthlem13 8485  pilem2 8610  pilem3 8611  bcsALT 8985  hhcms 9011  hlimcaui 9045  hhsscms 9089  projlem26 9150  projlem27 9151  pjthlem10 9166  ococint 9235  spanpr 9443  osumlem2 9519  osumlem4 9521  pjorth 9554  adjeqt 9798  nmbdoplb 9887  nmcopexlem3 9891  nmcoplb 9896  nmbdfnlb 9916  nmcfnexlem3 9920  nmcfnlb 9925  nmopco 9966  branmfnt 9976  hstnmoct 10088  mdsl0 10174  atoml 10246  atcvat4 10261  atabs 10265  infi1 10383  truni1 10422  hmphsyma 10451  hmphtr 10454  homcard 10462  fgsb2 10485  cnvtr 10518  rdmob 10561  cmpassoh 10609  homgrf 10610  cmpmon 10621  idmon 10624  immon 10625

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

Copyright terms: Public domain