Theorem sylancr 526

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancr.1	|- ((ph /\ ps) -> ch)
sylancr.2	|- ph
sylancr.3	|- (th -> ps)

Assertion

Ref	Expression
sylancr	|- (th -> ch)

Proof of Theorem sylancr

Step	Hyp	Ref	Expression
1		sylancr.2	. . 3 |- ph
2	1	a1i 8	. 2 |- (th -> ph)
3		sylancr.3	. 2 |- (th -> ps)
4		sylancr.1	. 2 |- ((ph /\ ps) -> ch)
5	2, 3, 4	syl11anc 524	1 |- (th -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  sbcel12gOLD 2553  sbceqdigOLD 2555  unipw 3504  difex2 3802  difex2OLD 3803  opeluu 3805  uniexb 3851  unon 3910  onuninsuci 3921  resiexg 4253  imaexg 4279  cnvexg 4424  coexg 4429  funssres 4460  cofunexg 4501  opabex2g 4540  fssxpOLD 4576  fcoi1OLD 4585  fcoi2OLD 4587  f1oabexg 4650  ssimaex 4729  dffv2 4734  fvopab6 4757  oprabex2g 4949  oprabval 4952  1stcof 5040  tz7.48-2 5166  tz7.49 5168  tz7.49c 5169  oawordeulem 5236  oeoalem 5271  oaabslem 5308  mapex 5387  ixpexg 5417  snfi 5491  sbthlem8 5517  phplem2 5603  onomeneq 5612  unblem4 5636  unfilem1 5641  pwfi 5661  tz9.12lem3 5772  tz9.12 5773  rankon 5782  bndrank 5793  rankbnd2 5815  rankxplim 5823  oncardval 5865  oncardon 5866  oncardid 5867  numth2 5947  numthcor 5948  zorn2lem2 5951  zorn 5959  brdom3 5963  unxpdom2 5997  sucxpdom 5998  alephfplem3 6046  cardcf 6059  nnaun 6089  distrlem4pr 6282  ltapr 6303  supsrlem1 6377  supsrlem2 6378  axmulopr 6418  axmulass 6431  axdistr 6432  cnegexlem2 6500  cnegex 6502  axmulgt0 6675  mnflt 6718  lediv12a 7079  recreclt 7085  posexi 7091  nnge1 7126  nnleltp1 7138  nnsubi 7140  nnaddm1cl 7142  xrsupsslem 7285  xrinfmsslem 7286  nn0ge0 7326  elnn0z 7356  zltp1le 7390  recnz 7403  modid 7512  fznn0 7694  fznn 7695  om2uzrani 7711  cardfz 7719  seq1rn2 7734  seq1seq02 7786  seqz1 7790  seq0p1 7794  seqzval2 7796  expge0 7833  expge1 7835  expubnd 7853  bernneq 7898  bernneqOLD 7899  bernneq2 7900  expnbnd 7901  discrlem3 7908  sqrlem12 7934  sqrlem17 7939  cjcl 8014  crre 8019  crim 8020  imre 8023  reim0 8024  mulre 8027  recj 8068  imcj 8069  cjreim 8078  cjreim2 8079  cj11OLD 8081  absreimsq 8107  absreim 8108  absdivzi 8110  cjdivi 8140  abs3lemi 8153  abs1mi 8156  seq1ublem 8163  seq1ubi 8164  cvg3i 8175  caubndi 8178  facdiv 8194  faclbnd2 8198  faclbnd3 8199  faclbnd4lem1 8200  faclbnd4lem3 8202  faclbnd5 8205  bccl2 8223  binomlem1 8326  binomlem2 8327  binomlem4 8329  binomlem5 8330  binomlem6 8331  clm4i 8340  clm0i 8343  climconsti 8354  climshfti 8364  iserzshft2i 8367  climrecl 8370  climmullem1 8380  climmullem2 8381  climmullem3 8382  climmullem4 8383  clim2serzi 8405  climubii 8413  climsupi 8415  climcaui 8416  caucvglem6 8422  caucvgi 8423  caucvg3ai 8424  caucvg3lem 8426  caucvg3 8428  serzf0i 8429  ser1clim0 8433  cvgcmp2lem 8440  cvgcmp2clem 8442  cvgcmp2clemOLD 8443  isumclimtfi 8456  isumshfti 8465  isumshft2i 8466  infcvglem1 8482  infcvglem3 8484  arisumi 8487  geoseri 8496  geolimilem 8497  georeclim 8502  geoisum 8504  geoisum1 8506  cvgratlem1ALT 8509  cvgratlem2ALT 8510  fsum0diaglem2 8519  cncfval 8526  ivthlem1 8543  ivthlem6 8548  ivthlem7 8549  efcltlem1 8566  ef0lem 8572  efcl 8574  efcvg 8576  efcvgfsum 8577  erelem1 8581  erelem2 8582  erelem3 8583  efaddlem1 8600  efaddlem5 8604  efaddlem6 8605  efaddlem23 8622  efaddlem26 8625  efaddlem27 8626  ef1tllem 8643  ef01tllem2 8646  ef01tllem2OLD 8647  abspef01tlubi 8660  efgt0i 8669  efcnlem1 8684  efcnlem2 8685  resinval 8698  recosval 8699  efi4p 8700  resin4p 8701  recos4p 8702  resincl 8703  recoscl 8704  efmival 8713  efeul 8714  subcos 8725  cos2tsin 8729  sin01bndlem2 8734  sin01bndlem3 8735  cos01bndlem2 8736  cos01bndlem3 8737  cos01gt0 8743  absef 8749  absefib 8750  efieq1re 8751  demoivre 8752  acdc3lem 8754  acdclem 8763  znnenlem 8770  znnen 8771  unbenlem 8773  infpnlem2 8776  infxpidmlem12 8832  infunabs 8834  infcda 8836  infdif 8837  infpss 8843  unctb 8846  infmap2 8850  alephadd 8851  alephexp1 8853  gch-kn 8856  tgval3 8895  metgt0 9097  metxplem3 9105  metxp 9111  tgioolem 9192  lmfval 9203  lmbr 9206  lmconst 9212  lmnn 9213  iscau 9214  metelcls 9243  bopcnlem4 9262  bcthlem7 9283  bcthlem16 9292  bcthlem18 9294  bcthlem20 9296  bcthlem22 9298  bcthlem23 9299  bcthlem28 9304  bcthlem33 9309  isgrp2i 9360  issubgi 9431  ghgrpilem3 9443  ghgrpilem4 9444  ghgrpi 9445  gaid 9454  isvc 9532  nvvop 9560  ubthlem5 9876  oprabco 10159  dif1enOLD 10173  findcardOLD 10179  tx1cn 10223  tx2cn 10224  txcn 10227  on1el4 10413  ring1cl 10415  bnj1494 13162  bnj102 13222  bnj149 13241  bnj1367 13511  tfisg 13912  trcltr 13936  frxp 13951  poseq 13954  wfrlem13 13969  wfrlem15 13971  sltval2 13997  axdenselem3 14021  axdenselem6 14024  nocvxminlem 14028  nocvxmin 14029  axfelem3 14033  axfelem4 14034  axfelem5 14035  axfelem14 14044  altxpexg 14101  inpreima5 14469  dfdir2 14639  isdir2 14640  clfsebs2 14710  seqzp2 14716  fnopabco2b 14734  trset 14756  imtr 14762  unint2t 14866  limvinlv 14941  trhom 14983  cntrsetlem 14999  supexr 15043  dualded 15132  dualcat2 15133  tclinf 15241  cptarc 15242  vtarsu 15263  isline1 15294  cover2 15673  opabex3 15701  fnopabco 15711  oprabexd 15713  upixp 15729  findcard2 15745  fimax 15746  rddif 15798  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  incsequz 15815  seq1eq2 15817  fsumltisumi 15823  csbrni 15832  trirni 15833  neificl 15841  mettrifi 15847  mettrifi2 15848  geomcau 15849  iirev 15871  iccst 15875  icoopnst 15876  iocopnst 15877  tlmval 15903  tlmconst 15907  ismtyval 15947  heiborlem6 15960  heiborlem8 15962  heiborlem10 15964  heiborlem11 15965  heiborlem15 15969  heiborlem18 15972  heiborlem21 15975  heiborlem27 15981  heiborlem28 15982  heiborlem32 15986  heiborlem33 15987  heiborlem35 15989  bfplem6 16003  bfplem7 16004  bfplem8 16005  bfplem9 16006  bfp 16009  recms 16010  rrncms 16019  rrntotbnd 16022  reheibor 16025  iccbnd 16026  pcoass 16085  pcorev 16087  isringd 16097  ee01an 16584  unipwr 16657  pmod 17311

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

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain