Theorem syld 44

Description: Syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Notice that syld 44 has the same form as syl 16 with ph added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace ph with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 22 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible.

Hypotheses

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

Assertion

Ref	Expression
syld	|- ( ph -> ( ps -> th ) )

Proof of Theorem syld

Step	Hyp	Ref	Expression
1		syld.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syld.2	. . 3 |- ( ph -> ( ch -> th ) )
3	2	a1d 25	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpdd 40	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  3syld  55  sylsyld  56  nsyld  140  pm2.61d  158  sylibd  214  sylbid  215  sylibrd  234  sylbird  235  syland  479  a2andOLD  810  ax12v  1863  alrimdd  1888  axc112  1945  nfeqf2  2047  sbequi  2120  2eu1  2307  axext3  2362  trel3  4468  poss  4716  sess2  4762  wefrc  4787  wereu2  4790  funun  5538  ssimaex  5839  f1imass  6073  soisoi  6125  isores3  6132  isofrlem  6137  isoselem  6138  weniso  6151  oninton  6534  orduniorsuc  6564  limuni3  6586  tfindsg  6594  limom  6614  f1o2ndf1  6807  soxp  6812  extmptsuppeq  6842  smoel  6949  smogt  6956  tfrlem9  6972  tz7.49  7028  seqomlem1  7033  odi  7146  omass  7147  omeulem2  7150  oeordsuc  7161  oeeulem  7168  ertr  7244  swoord2  7259  ecopovtrn  7332  domtriord  7582  onomeneq  7626  unxpdomlem2  7641  isinf  7649  pssnn  7654  findcard3  7678  frfi  7680  unblem3  7689  dffi3  7806  en3lplem1  7945  inf3lem3  7961  inf3lem5  7963  noinfep  7990  cantnfle  8003  cantnfp1lem3  8012  cantnfleOLD  8033  cantnfp1lem3OLD  8038  rankxpsuc  8213  tcrank  8215  ficardom  8255  carduni  8275  infxpenlem  8304  dfac8alem  8323  ac10ct  8328  ween  8329  alephdom  8375  alephle  8382  iscard3  8387  alephfp  8402  cdainf  8485  pwsdompw  8497  infdif  8502  cfslbn  8560  cofsmo  8562  cfsmolem  8563  cfcof  8567  fin1a2s  8707  domtriomlem  8735  ac6num  8772  zorn2lem3  8791  axdclem2  8813  imadomg  8825  iundom2g  8828  ficard  8853  fpwwe2lem8  8926  fpwwe2  8932  gchaclem  8967  tskr1om2  9057  inar1  9064  tskord  9069  tskuni  9072  grudomon  9106  grur1a  9108  grur1  9109  addnidpi  9190  ltexnq  9264  genpnnp  9294  addclprlem2  9306  mulclprlem  9308  psslinpr  9320  ltaddpr2  9324  ltexprlem6  9330  ltexprlem7  9331  addcanpr  9335  mulgt0sr  9393  map2psrpr  9398  supsrlem  9399  axrrecex  9451  letr  9589  dedekind  9655  recex  10098  lemul12b  10316  mulgt1  10318  fimaxre2  10407  lbreu  10409  nnrecgt0  10490  nnunb  10708  bndndx  10711  zeo  10865  uzind  10871  fzind  10877  fnn0ind  10878  suprfinzcl  10894  suprzcl2  11091  zmax  11098  rpnnen1lem5  11131  xrletr  11282  qbtwnre  11319  qsqueeze  11321  qextltlem  11322  xralrple  11325  xlesubadd  11376  supxrunb1  11432  icoshft  11563  fzen  11624  elfz1b  11670  elfz0fzfz0  11701  elfzmlbmOLD  11707  elfzmlbp  11708  fzo1fzo0n0  11759  elfzo0z  11760  fzofzim  11764  elfzodifsumelfzo  11781  ssfzoulel  11805  modadd1  11934  modmul1  11943  uzrdgfni  11972  fsuppmapnn0fiub0  12002  fsuppmapnn0ub  12004  fsuppmapnn0fz  12005  seqcl2  12028  seqfveq2  12032  seqshft2  12036  monoord  12040  seqsplit  12043  seqf1olem1  12049  seqf1olem2  12050  seqid2  12056  seqhomo  12057  expnbnd  12197  faclbnd4lem4  12276  seqcoll  12416  swrdsbslen  12584  swrdspsleq  12585  swrdswrdlem  12595  swrdswrd  12596  reuccats1lem  12616  swrdccatin12lem2a  12621  swrdccatin12lem2b  12622  swrdccatin12lem3  12626  swrdccat3a  12630  swrdccat3blem  12631  repswswrd  12667  swrd2lsw  12801  sqeqd  13001  sqrmo  13087  cau3lem  13189  limsupbnd2  13308  lo1bdd2  13349  climuni  13377  rlimcn2  13415  mulcn2  13420  o1of2  13437  rlimo1  13441  lo1le  13476  isercolllem1  13489  iseralt  13509  cvgrat  13694  fprodss  13757  rpnnen2  13961  ruclem3  13968  sqrt2irr  13984  dvds2lem  13998  dvdslelem  14032  divalglem8  14060  bitsinv1lem  14093  sadcaddlem  14109  smu01lem  14137  smueqlem  14142  bezoutlem4  14181  algcvga  14210  isprm3  14228  coprm  14243  coprmdvds2  14246  isprm5  14255  rpexp12i  14265  phibndlem  14302  dfphi2  14306  eulerthlem2  14314  odzdvds  14324  iserodd  14361  pclem  14364  pcpremul  14369  pcqcl  14382  pcdvdsb  14394  pcprmpw2  14407  pcaddlem  14409  pcmptcl  14412  pcfac  14420  prmpwdvds  14424  unbenlem  14428  prmreclem1  14436  4sqlem17  14481  vdwmc2  14499  vdwlem9  14509  vdwlem10  14510  vdwlem13  14513  vdwnnlem3  14517  ramcl  14549  mreiincl  15003  initoid  15401  termoid  15402  initoeu1  15407  initoeu2lem1  15410  termoeu1  15414  pospo  15720  dirge  15984  gsmsymgrfixlem1  16569  oddvdsnn0  16685  oddvds  16688  odcl2  16704  gexdvds  16721  sylow1lem1  16735  sylow2alem2  16755  sylow2a  16756  efgi2  16860  efgsrel  16869  efgs1b  16871  cyggex2  17016  telgsums  17135  pgpfac1lem2  17239  pgpfac1lem3a  17240  pgpfac1lem3  17241  pgpfac1lem5  17243  lssssr  17712  cply1mul  18448  gsummoncoe1  18459  gzrngunitlem  18595  znunit  18693  frgpcyg  18703  lsmcss  18814  obselocv  18850  obslbs  18852  scmataddcl  19103  scmatsubcl  19104  cpmatacl  19302  cpmatinvcl  19303  cpmatmcllem  19304  m2cpminvid2lem  19340  mp2pm2mplem4  19395  pm2mp  19411  chfacfisf  19440  chfacfisfcpmat  19441  chfacfscmul0  19444  chfacfpmmul0  19448  cayhamlem4  19474  ordtrest2lem  19790  leordtval2  19799  lecldbas  19806  cncls  19861  cncnp  19867  cnpresti  19875  lmcnp  19891  cnt0  19933  isreg2  19964  cmpsublem  19985  cmpsub  19986  tgcmp  19987  bwth  19996  dfcon2  20005  1stcfb  20031  2ndcctbss  20041  1stcelcls  20047  islly2  20070  dislly  20083  reftr  20100  comppfsc  20118  kgencn2  20143  txcnp  20206  txindis  20220  txcmplem1  20227  txlm  20234  xkohaus  20239  cnmptcom  20264  kqfvima  20316  isr0  20323  fgss2  20460  fbasrn  20470  filuni  20471  ufilmax  20493  isufil2  20494  cfinufil  20514  fmfnfmlem1  20540  fmfnfmlem2  20541  fmfnfmlem4  20543  fmfnfm  20544  fmco  20547  flimopn  20561  hausflim  20567  flimrest  20569  fclsopn  20600  flimfnfcls  20614  alexsubALTlem2  20633  alexsubALTlem3  20634  alexsubALT  20636  ptcmplem2  20638  cnextcn  20652  symgtgp  20685  qustgplem  20704  tsmsresOLD  20730  tsmsres  20731  tsmsxplem1  20740  isucn2  20867  imasdsf1olem  20961  bldisj  20986  blssps  21012  blss  21013  metcnp3  21128  ngptgp  21235  nrginvrcn  21285  nmoleub  21323  xrsmopn  21402  icccmplem3  21414  reconnlem2  21417  rectbntr0  21422  rescncf  21486  iocopnst  21525  iccpnfcnv  21529  lebnumii  21551  nmoleub2lem  21682  nmhmcn  21688  fgcfil  21795  iscfil3  21797  iscau2  21801  iscau3  21802  iscau4  21803  iscmet3lem2  21816  cfilres  21820  caussi  21821  equivcfil  21823  equivcau  21824  ivthlem2  21949  ivthlem3  21950  ovoliunlem2  21999  ovoliunnul  22003  ovolicc2lem3  22015  ioombl1lem4  22056  dyadmax  22092  dyadmbl  22094  volsup2  22099  itg2le  22231  itg2const2  22233  itg2seq  22234  itgsplitioo  22329  dvnres  22419  rolle  22476  c1lip1  22483  dvivthlem1  22494  lhop1  22500  dvcnvrelem1  22503  dvfsumrlim  22517  ply1divmo  22621  ig1peu  22657  plypf1  22694  coeaddlem  22731  fta1  22789  quotcan  22790  aalioulem4  22816  ulmcaulem  22874  ulmcn  22879  pilem2  22932  sincosq1lem  22975  sinq12gt0  22985  sinq12ge0  22986  sineq0  22999  tanord1  23009  lognegb  23062  logrec  23221  dcubic  23293  xrlimcnp  23415  o1cxp  23421  ftalem2  23464  ftalem3  23465  fsumdvdscom  23578  chtub  23604  vmasum  23608  bcmono  23669  bposlem3  23678  bposlem7  23682  lgsdir  23722  lgsqrlem2  23734  lgsdchr  23740  lgsquadlem2  23747  2sqlem6  23761  dchrisumlem3  23793  pntrsumbnd2  23869  pntpbnd1  23888  pntibnd  23895  pntlem3  23911  pntleml  23913  brbtwn2  24329  colinearalg  24334  axcontlem10  24397  redwlk  24729  usgra2adedgspthlem2  24733  fargshiftf1  24758  constr3trllem2  24772  4cycl4dv  24788  usg2wlkeq  24829  wwlknred  24844  wwlknextbi  24846  wwlkm1edg  24856  clwlkswlks  24879  clwlkisclwwlklem2fv2  24904  clwlkisclwwlklem2a  24906  clwlkisclwwlklem1  24908  clwwlkf  24915  clwwlkext2edg  24923  wwlksubclwwlk  24925  clwwisshclwwlem1  24926  usg2wotspth  25005  vdusgra0nedg  25029  usgravd0nedg  25039  usgravd00  25040  eupath2  25101  frgraregorufrg  25193  numclwwlkovf2ex  25207  numclwlk1lem2foa  25212  numclwlk1lem2fo  25216  ex-natded5.3-2  25250  isgrpo  25315  opidonOLD  25441  vacn  25721  ubthlem2  25904  htthlem  25951  normgt0  26161  shmodsi  26424  spansneleq  26605  h1datomi  26616  pjjsi  26735  nmcexi  27061  pjnormssi  27203  stm1add3i  27282  golem2  27307  cvnsym  27325  dmdmd  27335  mdslmd1lem1  27360  mdslmd1i  27364  mdexchi  27370  atcveq0  27383  superpos  27389  hatomistici  27397  atoml2i  27418  atcvat2i  27422  chirredlem1  27425  atcvat3i  27431  mdsymlem3  27440  mdsymlem5  27442  cdj3lem2b  27472  cdj3i  27476  supssd  27675  2sqmod  27789  resspos  27800  resstos  27801  submarchi  27883  tpr2rico  28048  ordtrest2NEWlem  28058  xrge0iifcnv  28069  omssubadd  28427  eulerpartlemb  28490  ballotlemfc0  28614  ballotlemfcc  28615  subfacp1lem6  28818  iccllyscon  28884  cvmfolem  28913  cvmliftlem7  28925  cvmliftlem10  28928  ghomf1olem  29223  fundmpss  29362  dfon2lem3  29382  dfon2lem6  29385  axext4dist  29398  setlikess  29440  trpredtr  29478  trpredmintr  29479  dftrpred3g  29481  trpredrec  29486  frmin  29487  soseq  29499  wfrlem12  29519  frrlem5e  29560  frrlem11  29564  sltval2  29581  sltres  29589  nodenselem4  29609  nodenselem8  29613  nobndlem6  29622  dfrdg4  29753  5segofs  29809  cgrextend  29811  segconeu  29814  btwncomim  29816  btwnswapid  29820  btwnintr  29822  btwnexch3  29823  btwndiff  29830  ifscgr  29847  cgrxfr  29858  btwnxfr  29859  lineext  29879  brofs2  29880  linecgr  29884  lineid  29886  idinside  29887  endofsegid  29888  btwnconn1lem13  29902  btwnconn3  29906  onsuct0  30059  limsucncmpi  30063  wl-aetr  30148  fin2so  30205  tan2h  30212  heicant  30214  mblfinlem2  30217  mblfinlem3  30218  itg2addnclem  30232  itg2addnclem2  30233  itg2gt0cn  30236  ftc1anclem5  30260  ftc1anclem6  30261  finminlem  30302  nn0prpwlem  30306  cldbnd  30310  clsint2  30313  fnessref  30341  neibastop3  30346  fgmin  30354  filbcmb  30397  nninfnub  30410  mettrifi  30416  geomcau  30418  istotbnd3  30433  sstotbnd2  30436  ismtybndlem  30468  heibor1lem  30471  heiborlem1  30473  heiborlem8  30480  heiborlem10  30482  heibor  30483  riscer  30557  crngohomfo  30569  keridl  30595  ispridl2  30601  ispridlc  30633  ac6s6  30746  fphpdo  30916  icodiamlt  30921  pellexlem5  30934  pellexlem6  30935  jm2.26lem3  31109  dfac21  31178  unxpwdom3  31207  ordpss  31528  stoweidlem34  31982  pfxccatin12lem1  32598  reuccatpfxs1lem  32608  ralralimp  32616  zm1nn  32646  ltsubnn0  32648  elfz2z  32652  usgedgimp  32721  usgvincvad  32722  usgedgimpALT  32724  usgvincvadALT  32725  zrtermorngc  33009  zrtermoringc  33078  ztprmneprm  33136  lcosslsp  33239  lindslinindsimp1  33258  lindslinindsimp2lem5  33263  snlindsntor  33272  m1modmmod  33334  flnn0div2ge  33350  aacllem  33550  19.41rg  33663  bj-exalimi  34572  dral1-o  35046  ax12indalem  35088  ax12inda2ALT  35089  lsatcveq0  35170  eqlkr3  35239  atlatmstc  35457  atlrelat1  35459  hlrelat2  35540  intnatN  35544  cvrexchlem  35556  cvratlem  35558  cvrat2  35566  atltcvr  35572  cvrat3  35579  cvrat4  35580  ps-1  35614  ps-2  35615  lplnnle2at  35678  lvolnle3at  35719  2llnma3r  35925  cdlemblem  35930  pmapjoin  35989  elpcliN  36030  lhpmcvr4N  36163  4atexlemnclw  36207  trlnidatb  36315  cdlemc4  36332  cdlemd3  36338  cdleme3g  36372  cdleme7d  36384  cdleme11c  36399  cdleme11dN  36400  cdleme21b  36465  cdleme21c  36466  cdleme21i  36474  cdleme22b  36480  cdleme35fnpq  36588  cdlemf1  36700  trlord  36708  cdlemg6c  36759  dihglblem6  37480  dochlkr  37525  dochkrshp  37526  dihjat1lem  37568  dochexmidlem5  37604  dochexmidlem8  37607  ov2ssiunov2  38219