Theorem syldan 516

Description: A syllogism deduction with conjoined antecents.

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	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 402	. . 3 |- (ph -> (ps -> ch))
3		syldan.2	. . . 4 |- ((ph /\ ch) -> th)
4	3	ex 402	. . 3 |- (ph -> (ch -> th))
5	2, 4	syld 30	. 2 |- (ph -> (ps -> th))
6	5	imp 377	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  csbnest1g 2582  elpw2g 3463  mouniss 3816  elpwunsn 3856  fnbr 4515  fnexALT 4536  dffv2 4734  tfr3 5134  tz7.48-2 5166  omlimcl 5257  ixpexg 5417  ac6sfi 5509  fofi 5658  iunfi 5659  omsubindss 5888  ltaddpr 6292  ltexprlem7 6300  1idsr 6359  addgt0sr 6365  pm2.61ltlei 6705  mulgt1 7027  lediv1OLD 7034  gt0div 7035  ge0div 7036  ltrec1 7071  lerec2 7072  lediv2 7074  lediv12a 7079  recreclt 7085  nn2ge 7125  lbinfm 7257  xrsupsslem 7285  xrinfmsslem 7286  supxr 7290  supxr2 7291  supxrpnf 7297  supxrunb1 7298  supxrunb2 7299  recnz 7403  modcl 7502  modge0 7503  zmodcl 7511  uzwo2 7626  fznn0sub2 7671  expord2 7849  exple1 7852  le2sq2 7877  expnbnd 7901  expnlbnd2 7903  leabs 8115  absmax 8149  faclbnd4lem3 8202  bcval4 8213  fsum1s2 8270  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  fsumrev 8289  fsummulc1 8293  fsumcmp 8300  fsumcmpndx2 8302  fsumabs 8303  climconsti 8354  climaddc2 8379  climmullem5 8384  climmullem8 8387  clim2serz 8394  clim2serzi 8405  iserzexi 8406  isumclim3 8461  isumclim5 8463  isum1p 8467  isumrecl 8471  georeclim 8502  geoisumr 8505  cvgratlem5 8516  fsum0diaglem2 8519  cncffvrn 8535  efaddlem6 8605  reeff1o 8691  unbenlem 8773  infdif 8837  tgcl 8894  basgen2 8909  opncld 8950  iincld 8955  uncld 8957  ntrval2 8962  clsss3 8967  ntrss3 8968  clsidm 8974  ntridm 8975  opnssneib 9005  ssnei2 9006  neindisj 9007  innei 9012  cnpnei 9043  dnsconst 9065  metxptval 9107  ssblex 9133  opni2 9142  metequiv 9158  metcn 9167  metcnpi3 9170  metcnpi4 9171  cncfmet 9183  lmnn 9213  lmsslem 9230  metelcls 9243  cmsss 9275  bcthlem21 9297  grpidinvlem2 9329  grpidinvlem3 9330  grpideu 9333  grpinvid1 9356  grpinvid2 9357  grplcan 9359  grp2inv 9363  grpinvop 9365  grpmuldivass 9373  grppnpcan2 9377  grpnnncan2 9378  grpnpncan 9379  gxinv 9393  grplactf1o 9406  abl4 9413  ablmuldiv 9415  abldivdiv4 9417  ablnnncan 9419  ablnnncan1 9421  ghgrpilem3 9443  ringlz 9487  ringrz 9488  vc0 9520  vcz 9521  nvzs 9597  nvmdi 9602  nvnegneg 9603  nvsubadd 9607  nvnpcan 9612  nvmeq0 9616  nvabs 9633  nvlmle 9665  sspmval 9731  sspz 9733  sspival 9736  sspimsval 9738  lnoadd 9758  lnosub 9759  lnomul 9760  nmoub3i 9775  0lno 9790  nmblolbii 9799  blocnilem 9804  blocni 9805  ipsubdir 9849  sspph 9856  ubthlem9 9880  ubthlem12 9883  ubthlem12OLD 9884  ubthlem13 9885  ubthlem13OLD 9886  ubthlem14 9887  pstr 9995  efifolem7 10082  txcnopab 10228  fbunfip 10282  hausfillim 10303  elfilmap3 10314  flimfnei 10319  fbaslim 10322  tosdir 10358  hvaddsub4 10578  hi2eq 10604  chocunii 10805  projlem26 10844  shsel3 10912  chabs1 11072  pjspansn 11133  5oalem2 11235  3oalem2 11243  pjoi0 11297  nmopub2tALT 11470  nmfnleub2 11487  elnlfn2 11490  eigvalcl 11522  eighmre 11524  leopmul 11705  nmopleid 11710  spansncv2 11865  chcv1 11927  atcv0eq 11951  atexch 11953  irredi 11966  cdj1i 12005  bnj594 13300  lediv2aALT 13621  ghomf1olem 13637  gcdcllem1 13718  mulgcdlem2 13757  zgt1b1 13771  dfon2lem9 13857  sltval2 13997  findabrcl 14255  fprod1s2 14678  grpdrcan 14738  invaddvec 14810  dblsubvec 14817  mvecrtol2 14820  qusp 14908  msr4 15004  mslb1 15007  lvsovso3 15040  dmrngcmp 15098  tarsin 15230  tarone 15232  tarmrtwo 15234  vtarsu 15263  omsubindssOLD 15397  opnregcld 15415  cldregopn 15416  opnnei 15417  cnsubsp2 15427  cptclsscpt 15432  dfcon2 15442  connsub 15443  cnconn 15444  isfne 15480  topfneec 15501  topjoin 15527  limfilcf 15587  flimcls 15588  fmfnfmlem1 15594  istail 15634  eropreu 15733  eroprf 15735  infmrlb 15765  fisup2g 15768  pofun 15772  fzsplit 15792  absrdbnd 15799  sdc 15811  fdc 15812  subspcld2 15839  metf1o 15843  icoopnst 15876  iocopnst 15877  cnimass 15888  cnresima 15891  cnss 15892  paste 15893  piececn 15894  tlmconst 15907  lmtlm 15908  sstotbnd 15936  isbnd3 15941  bndss 15942  heiborlem19 15973  heiborlem36 15990  rrncms 16019  reheibor 16025  abl4pnp 16037  ghomdiv 16041  pcoass 16085  pcorev 16087  pi1gp 16095  ringneglmul 16104  ringnegrmul 16105  ringsubdi 16106  ringsubdir 16107  isdivrng2 16111  rnghomco 16128  rngisoco 16136  iscringd 16147  crngm4 16151  idlsubcl 16171  divrngidl 16176  unichnidl 16179  keridl 16180  maxidln1 16192  maxidln0 16193  igenidl 16211  igenidl2 16213  ispridlc 16218  dmncan1 16224  strdif 16719  latjlej1 16866  latmlem1 16876  latledi 16884  latj23 16887  latm12 16955  cvrle 16995  cvrnle 16997  cvrne 16998  cvrntr 17063  grpidinvlem2NEW 17110  grpidinvlem3NEW 17111  grpideuNEW 17114  grpinvid1NEW 17131  grpinvid2NEW 17132  grplcanNEW 17134  ringlzNEW 17156  ringrzNEW 17157  linepsub 17232  paddasslem17 17297  polval2 17319  polssat 17321  polpmap 17324  2polpmap 17325  2polval 17326  2polss 17327  3pol 17328  2pmaplub 17336  polat 17341  2polat 17342  pmapidcl 17351  ispsubcl2 17356  linepsubcl 17359  polsubcl 17360  psubclsub 17387

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