Theorem syldan 691

Description: A syllogism deduction with conjoined antecents. (The proof was shortened by Wolf Lammen, 6-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
syldan	|- ((ph /\ ps) -> th)

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. 2 |- ((ph /\ ps) -> ch)
2		syldan.2	. . . 4 |- ((ph /\ ch) -> th)
3	2	expcom 495	. . 3 |- (ch -> (ph -> th))
4	3	adantrd 548	. 2 |- (ch -> ((ph /\ ps) -> th))
5	1, 4	mpcom 105	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 433

This theorem is referenced by:  sylan2 696  sylan2OLD 705  csbnest1g 2845  elpw2g 3662  pofun 3795  mouniss 3986  elpwunsn 4034  fnbr 4653  fnexALT 4671  dffv2 4859  tfr3 5338  tz7.48-2 5369  tz7.48-2OLD 5370  omlimcl 5460  ixpexg 5621  omxpenlem 5712  ac6sfi 5718  fofi 5926  iunfi 5927  fisup2g 5952  infxpenlem 6212  omsubindss 6244  axdc3lem2 6377  ltaddpr 6735  ltexprlem7 6743  1idsr 6802  addgt0sr 6808  pm2.61ltlei 6995  mulgt1 7461  lediv1OLD 7469  gt0div 7470  ge0div 7471  ltdiv2 7505  ltrec1 7506  lerec2 7507  lediv2 7509  lediv12a 7514  recreclt 7520  nn2ge 7560  lbinfm 7705  xrsupsslem 7737  xrinfmsslem 7738  supxr 7742  supxr2 7743  supxrpnf 7749  supxrunb1 7750  supxrunb2 7751  recnz 7858  modcl 7960  modge0 7961  zmodcl 7969  uzwo2 8087  fznn0sub2 8148  expord2 8349  exple1 8352  le2sq2 8377  expnbnd 8401  expnlbnd2 8403  leabs 8615  absmax 8650  faclbnd4lem3 8703  bcval4 8714  fsum1s2 8782  fsum1ps 8790  fsumsplit 8792  fsumadd 8794  fsumrev 8801  fsummulc1 8805  fsumcmp 8812  fsumcmpndx2 8814  fsumabs 8815  climconsti 8866  climaddc2 8891  climmullem5 8896  climmullem8 8899  clim2serz 8906  clim2serzi 8917  iserzexi 8918  isumclim3 8973  isumclim5 8975  isum1p 8979  isumrecl 8983  georeclim 9018  geoisumr 9021  cvgratlem5 9032  fsum0diaglem2 9035  cncffvrn 9051  efaddlem6 9121  reeff1o 9207  rpnnen1lem5 9293  rpnnen2lem10 9304  rpnnen2lem11 9305  infdif 9367  gcdcllem1 9448  mulgcdlem2 9488  unbenlem 9522  grpidinvlem2 9621  grpidinvlem3 9622  grpideu 9625  grpinvid1 9646  grpinvid2 9647  grplcan 9649  ringlz 9671  ringrz 9672  latjlej1 9777  latmlem1 9793  latledi 9801  latj32 9809  latjjdi 9815  tgcl 9895  basgen2 9910  opncld 9961  iincld 9968  uncld 9970  ntrval2 9976  clsss3 9981  ntrss3 9982  clsidm 9988  ntridm 9989  opnssneib 10020  ssnei2 10021  neindisj 10022  opnnei 10025  innei 10028  cnpnei 10059  dnsconst 10081  metxptval 10123  ssblex 10149  opni2 10158  metequiv 10174  metcn 10183  metcnpi3 10186  metcnpi4 10187  cncfmet 10199  lmnn 10229  lmsslem 10246  metelcls 10259  metelclsOLD 10260  cmsss 10293  bcthlem21 10315  grpoidinvlem2 10350  grpoidinvlem3 10351  grpoideu 10354  grpoinvid1 10377  grpoinvid2 10378  grpolcan 10380  grp2inv 10384  grpinvop 10386  grpmuldivass 10394  grppnpcan2 10398  grpnnncan2 10399  grpnpncan 10400  gxinv 10414  grplactf1o 10427  abl4 10434  ablmuldiv 10436  abldivdiv4 10438  ablnnncan 10440  ablnnncan1 10442  ghgrpilem3 10464  ringolz 10508  ringorz 10509  vc0 10541  vcz 10542  nvzs 10618  nvmdi 10623  nvnegneg 10624  nvsubadd 10628  nvnpcan 10633  nvmeq0 10637  nvabs 10654  nvlmle 10686  sspmval 10752  sspz 10754  sspival 10757  sspimsval 10759  lnoadd 10779  lnosub 10780  lnomul 10781  nmoub3i 10796  0lno 10813  nmblolbii 10822  blocnilem 10827  blocni 10828  ipsubdir 10872  sspph 10879  ubthlem9 10903  ubthlem12 10906  ubthlem12OLD 10907  ubthlem13 10908  ubthlem13OLD 10909  ubthlem14 10910  pstr 11022  efifolem7 11109  txcnopab 11221  fbunfip 11278  hausfillim 11299  elfilmap3 11310  flimfnei 11315  fbaslim 11318  tosdir 11354  hvaddsub4 11573  hi2eq 11599  chocunii 11797  projlem26 11836  shsel3 11904  chabs1 12064  pjspansn 12125  5oalem2 12225  3oalem2 12233  pjoi0 12287  nmopub2tALT 12460  nmfnleub2 12477  elnlfn2 12480  eigvalcl 12512  eighmre 12514  leopmul 12694  nmopleid 12699  spansncv2 12854  chcv1 12916  atcv0eq 12940  atexch 12942  irredi 12955  cdj1i 12994  bnj594 14229  ghomf1olem 14621  sindivcvglem2 14634  lediv2aALT 14660  dfon2lem9 14738  sltval2 14909  findabrcl 15202  fprod1s2 15678  grpdrcan 15734  ltrinvlem 15766  invaddvec 15824  dblsubvec 15831  mvecrtol2 15834  intopcoaconb 15923  qusp 15932  msr4 16057  mslb1 16060  lvsovso3 16095  dmrngcmp 16153  tarsin 16301  tarone 16303  tarmrtwo 16305  vtarsu 16334  omsubindssOLD 16482  opnregcld 16500  cldregopn 16501  opnneiOLD 16502  cnsubsp2 16512  cptclsscpt 16517  dfcon2 16527  connsub 16528  cnconn 16529  isfne 16565  topfneec 16586  topjoin 16612  limfilcf 16672  flimcls 16673  fmfnfmlem1 16679  istail 16719  eropreu 16818  eroprf 16820  infmrlb 16850  fisup2gOLD 16853  pofunOLD 16857  fzsplit 16877  absrdbnd 16884  sdc 16896  fdc 16897  subspcld2 16924  metf1o 16928  icoopnst 16961  iocopnst 16962  cnimass 16973  cnresima 16976  cnss 16977  paste 16978  piececn 16979  tlmconst 16992  lmtlm 16993  sstotbnd 17021  isbnd3 17026  bndss 17027  heiborlem19 17058  heiborlem36 17075  rrncms 17104  reheibor 17110  abl4pnp 17122  ghomdiv 17126  pcoass 17170  pcorev 17172  pi1gp 17180  ringneglmul 17189  ringnegrmul 17190  ringsubdi 17191  ringsubdir 17192  isdivrng2 17196  rnghomco 17213  rngisoco 17221  iscringd 17232  crngm4 17236  idlsubcl 17256  divrngidl 17261  unichnidl 17264  keridl 17265  maxidln1 17277  maxidln0 17278  igenidl 17296  igenidl2 17298  ispridlc 17303  dmncan1 17309  olm11 17883  latm12 17886  cvrle 17931  cvrnle 17933  cvrne 17934  cvrval3 18073  atcvrj0 18088  atltcvr 18095  atbtwnexOLD 18108  atbtwnex 18109  3at 18151  2atneat 18215  llncvrlpln2 18261  lplncvrlvol2 18319  dalemdnee 18370  linepsub 18456  isline2 18478  paddasslem17 18540  pmapjlln1 18559  polval2 18595  polssat 18597  polpmap 18600  2polpmap 18601  2polval 18602  2polss 18603  3pol 18604  2pmaplub 18612  polat 18617  2polat 18618  psubclsub 18626  pmapidcl 18628  ispsubcl2 18633  linepsubcl 18636  polsubcl 18637  lhpoc2 18695  ltrncnvatb 18771  ltrnel 18772  trlval2 18794  trlval2OLD 18795  trljat1 18798  trljat2 18799  cdleme3b 18896

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 232  df-an 435

Copyright terms: Public domain