Theorem sylc 83

Description: A syllogism inference combined with contraction.

Hypotheses

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

Assertion

Ref	Expression
sylc	|- (ph -> th)

Proof of Theorem sylc

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

Syntax hints:   -> wi 3

This theorem is referenced by:  syl3c 84  pm2.65d 151  jc 153  jaod 469  sylancOLD 523  syl11anc 524  ee11 1268  ee222 1271  ee333 1279  elex22 2303  elex2 2304  sbc5gOLD 2471  sbc6gOLD 2473  tz7.7 3684  reuuniss2 3817  rabsnt 3821  euexeqOLD 3826  euexaleq 3827  ssorduni 3870  ssorduniOLD 3871  suceloni 3894  nlimsucg 3923  unielrel 4418  zfrep6 4545  oprabval3 4959  curry1 5075  curry2 5078  reiotass2 5111  tfrlem13 5131  th3q 5376  f1oen2g 5453  ac6sfi 5509  domnsym 5526  limensuci 5600  unfilem3 5643  supmax 5679  ordiso 5683  ordtypelem6 5689  inf3lem7 5725  noinfep 5747  r1val1 5769  omsubsuc 5877  omsubsdomlem2 5880  omsubsdom 5881  elomsubsd 5885  omsublim 5887  omsubindss 5888  infenomsub 5889  omsubinit 5890  imadomg 5968  unidom 5970  ltexpri 6301  prlem936 6307  recexpr 6312  supexpr 6315  lemul12a 7026  lemulge11 7030  nngt0 7129  nnaddm1cl 7142  rpge0 7241  supxrunb1 7298  supxrunb2 7299  nn0ltp1le 7336  nn0ind-raph 7426  qbtwnre 7459  fldiv 7497  eliooord 7556  cardfz 7719  facavg 8207  climubii 8413  cvgcmpi 8445  cvgcmpubi 8446  reccnv 8479  erelem3 8583  efaddlem16 8615  efaddlem25 8624  eftabsi 8637  abspef01tlubi 8660  absefm1lei 8677  sin01bndlem2 8734  cos01bndlem2 8736  sin01gt0 8742  efieq1re 8751  ruclem33 8811  ruclem35 8813  metcnp 9165  tgioolem 9192  lmnn 9213  ssga 9455  vacnlem3 9669  nmcn3 9680  nmcnc 9681  ubthlem13 9885  ubthlem13OLD 9886  pilem2 10021  pilem3 10022  findcard 10178  uptx 10226  filrn 10293  limfil 10297  isfilmap 10308  elfilmap3 10314  sflimf 10318  opidon 10369  bcsiALT 10679  hhcms 10705  hlimcauii 10739  hhsscms 10783  projlem26 10844  projlem27 10845  pjthlem10 10861  ococin 10930  spanpr 11136  osumlem2 11214  osumlem4 11216  pjorthi 11249  adjeq 11496  nmbdoplbi 11586  nmcopexlem3 11590  nmcoplbi 11595  nmbdfnlbi 11615  nmcfnexlem3 11619  nmcfnlbi 11624  nmopcoi 11665  branmfn 11675  branmfnOLD 11676  hstnmoc 11795  mdsl0 11882  atomli 11954  atcvat4i 11969  atabsi 11973  bnj1379 13100  bnj580 13301  bnj999 13365  bnj1398 13515  orderseqlem 13953  wfrlem4 13960  wfrlem15 13971  axdenselem3 14021  axfelem1 14031  axfelem8 14038  axfelem9 14039  axfelem12 14042  axfelem13 14043  axfelem16 14046  infi1 14343  ordsuccl3 14432  inpreima5 14469  injsurinj 14487  ispr1 14496  isprj1 14505  prl 14512  jidd 14540  midd 14541  preoref22 14570  dupos1 14586  ubos2 14598  ubos 14599  supdefa 14605  geme2 14617  dfps2 14634  fprodadd 14713  gapm2 14732  trinv 14759  rnplrnml3 14768  zerdivemp1 14785  truni1 14849  truni3 14851  hmphsyma 14882  hmphtr 14885  homcard 14893  fgsb2 14925  cnvtrhom 14984  altretop 14997  cnvtr 15016  lvsovso 15038  supnuf 15041  rdmob 15095  dualalg 15131  dualcat2 15133  cmpassoh 15150  homgrf 15151  cmpmon 15164  idmon 15166  immon 15167  idsubfun 15206  tarax3d2 15225  cptarc 15242  cardtar 15281  fictb 15371  ordisoOLD 15374  ordtypelem6OLD 15380  omsubsucOLD 15386  omsubsdomlem2OLD 15389  omsubsdomOLD 15390  elomsubsdOLD 15394  omsublimOLD 15396  omsubindssOLD 15397  infenomsubOLD 15398  omsubinitOLD 15399  opncldf2 15403  opncldf3 15404  compcov 15429  alexsublem4 15440  reconnlem1 15446  reconnlem4 15449  reconnlem5 15450  ivthALT 15454  isfne3 15482  fnessref 15503  refssfne 15504  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  isufil2 15565  ufprim 15569  filssufillem 15570  ufinffr 15578  ufilen 15579  filcon 15580  limfilcf 15587  flimcls 15588  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem4 15597  sfcls 15604  filclus 15605  flimfnfcls 15615  sfclusf 15624  tailf 15633  istail 15634  filnetlem5 15644  filnet 15645  abrexdom 15739  indexdom 15754  heiborlem9 15963  heiborlem14 15968  zerdivemp1x 16108  sbiota1 16399  stbval 16731  latjass 16886  lubss 16897  omllaw5 16968  cmtcomlem 16969  cmtbr3 16975  omlfh3 16979  cvrexchlem 17059  cvrat4 17076  paddss12 17280  paddasslem2 17282  paddasslem4 17284  paddasslem6 17286  paddasslem12 17292  paddun 17337  poml4 17361  poml5 17362  osumcllem6 17369  pexmidlem6 17383  pl42lem2 17408  pl42lem3 17409

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

Copyright terms: Public domain