Theorem syld 44

Description: Syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by 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  478  alrimdd  1813  axc112  1868  cbv1hOLD  1962  nfeqf2  1988  equveliOLD  2038  sbequi  2063  sbiedOLD  2101  dral1-o  2205  ax12indalem  2247  ax12inda2ALT  2248  trel3  4381  poss  4630  sess2  4676  wefrc  4701  wereu2  4704  ordelord  4728  funun  5448  ssimaex  5744  f1imass  5964  soisoi  6006  isores3  6013  isofrlem  6018  isoselem  6019  weniso  6032  oninton  6400  orduniorsuc  6430  limuni3  6452  tfindsg  6460  limom  6480  f1dmex  6536  f1o2ndf1  6669  soxp  6674  extmptsuppeq  6702  smoel  6807  smogt  6814  tfrlem9  6830  tz7.49  6886  seqomlem1  6891  abianfp  6900  odi  7006  omass  7007  omeulem2  7010  oeordsuc  7021  oeeulem  7028  ertr  7104  swoord2  7119  ecopovtrn  7191  domtriord  7445  2pwuninel  7454  onomeneq  7488  unxpdomlem2  7506  isinf  7514  pssnn  7519  findcard3  7543  frfi  7545  unblem3  7554  dffi3  7669  en3lplem1  7808  inf3lem3  7824  inf3lem5  7826  noinfep  7853  cantnfle  7867  cantnfp1lem3  7876  cantnfleOLD  7897  cantnfp1lem3OLD  7902  rankxpsuc  8077  tcrank  8079  ficardom  8119  carduni  8139  infxpenlem  8168  dfac8alem  8187  ac10ct  8192  ween  8193  alephdom  8239  alephle  8246  iscard3  8251  alephfp  8266  cdainf  8349  pwsdompw  8361  infdif  8366  cfslbn  8424  cofsmo  8426  cfsmolem  8427  cfcof  8431  fin1a2s  8571  domtriomlem  8599  ac6num  8636  zorn2lem3  8655  axdclem2  8677  imadomg  8689  iundom2g  8692  ficard  8717  fpwwe2lem8  8792  fpwwe2  8798  gchaclem  8833  tskr1om2  8923  inar1  8930  tskord  8935  tskuni  8938  grudomon  8972  grur1a  8974  grur1  8975  addnidpi  9058  ltexnq  9132  genpnnp  9162  addclprlem2  9174  mulclprlem  9176  psslinpr  9188  ltaddpr2  9192  ltexprlem6  9198  ltexprlem7  9199  addcanpr  9203  mulgt0sr  9260  map2psrpr  9265  supsrlem  9266  axrrecex  9318  letr  9456  dedekind  9521  recex  9956  lemul12b  10174  mulgt1  10176  ledivmulOLD  10194  fimaxre2  10266  lbreu  10268  nnrecgt0  10347  nnunb  10563  bndndx  10566  zeo  10715  uzind  10721  fzind  10728  fnn0ind  10729  lbzbi  10931  suprzcl2  10933  zmax  10938  rpnnen1lem5  10971  xrletr  11120  qbtwnre  11157  qsqueeze  11159  qextltlem  11160  xralrple  11163  xlesubadd  11214  supxrunb1  11270  icoshft  11394  fzen  11454  elfz0fzfz0  11472  elfzmlbm  11477  elfzmlbp  11478  elfz1b  11511  fzo1fzo0n0  11572  elfzo0z  11573  fzofzim  11577  elfzodifsumelfzo  11588  ssfzoulel  11605  modadd1  11729  modmul1  11736  uzrdgfni  11765  seqcl2  11808  seqfveq2  11812  seqshft2  11816  monoord  11820  seqsplit  11823  seqf1olem1  11829  seqf1olem2  11830  seqid2  11836  seqhomo  11837  expnbnd  11977  faclbnd4lem4  12056  seqcoll  12200  swrdnd  12310  swrdvalodm2  12317  swrdswrdlem  12337  swrdswrd  12338  swrdccatin12lem2a  12360  swrdccatin12lem2b  12361  swrdccatin12lem3  12365  swrdccat3a  12369  swrdccat3blem  12370  repswswrd  12406  swrd2lsw  12536  sqeqd  12639  sqrmo  12725  cau3lem  12826  limsupbnd2  12945  lo1bdd2  12986  climuni  13014  rlimcn2  13052  mulcn2  13057  o1of2  13074  rlimo1  13078  lo1le  13113  isercolllem1  13126  iseralt  13146  isumrpcl  13289  cvgrat  13326  rpnnen2  13491  ruclem3  13498  sqr2irr  13514  dvds2lem  13528  dvdslelem  13560  divalglem8  13587  bitsinv1lem  13620  sadcaddlem  13636  smu01lem  13664  smueqlem  13669  bezoutlem4  13708  algcvga  13737  isprm3  13755  coprm  13769  coprmdvds2  13772  isprm5  13781  rpexp12i  13791  phibndlem  13828  dfphi2  13832  eulerthlem2  13840  odzdvds  13850  iserodd  13885  pclem  13888  pcpremul  13893  pcqcl  13906  pcdvdsb  13918  pcprmpw2  13931  pcaddlem  13933  pcmptcl  13936  pcfac  13944  prmpwdvds  13948  unbenlem  13952  prmreclem1  13960  4sqlem17  14005  vdwmc2  14023  vdwlem9  14033  vdwlem10  14034  vdwlem13  14037  vdwnnlem3  14041  ramcl  14073  mreiincl  14517  pospo  15126  dirge  15390  gsmsymgrfixlem1  15912  oddvdsnn0  16027  oddvds  16030  odcl2  16046  gexdvds  16063  sylow1lem1  16077  sylow2alem2  16097  sylow2a  16098  efgi2  16202  efgsrel  16211  efgs1b  16213  cyggex2  16353  pgpfac1lem2  16550  pgpfac1lem3a  16551  pgpfac1lem3  16552  pgpfac1lem5  16554  lssssr  16956  gzrngunitlem  17721  znunit  17838  frgpcyg  17848  lsmcss  17959  obselocv  17995  obslbs  17997  ordtrest2lem  18649  leordtval2  18658  lecldbas  18665  cncls  18720  cncnp  18726  cnpresti  18734  lmcnp  18750  cnt0  18792  isreg2  18823  cmpsublem  18844  cmpsub  18845  tgcmp  18846  bwth  18855  bwthOLD  18856  dfcon2  18865  1stcfb  18891  2ndcctbss  18901  1stcelcls  18907  islly2  18930  dislly  18943  kgencn2  18972  txcnp  19035  txindis  19049  txcmplem1  19056  txlm  19063  xkohaus  19068  cnmptcom  19093  kqfvima  19145  isr0  19152  fgss2  19289  fbasrn  19299  filuni  19300  ufilmax  19322  isufil2  19323  cfinufil  19343  fmfnfmlem1  19369  fmfnfmlem2  19370  fmfnfmlem4  19372  fmfnfm  19373  fmco  19376  flimopn  19390  hausflim  19396  flimrest  19398  fclsopn  19429  flimfnfcls  19443  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALT  19465  ptcmplem2  19467  cnextcn  19481  symgtgp  19514  divstgplem  19533  tsmsresOLD  19559  tsmsres  19560  tsmsxplem1  19569  isucn2  19696  imasdsf1olem  19790  bldisj  19815  blssps  19841  blss  19842  metcnp3  19957  ngptgp  20064  nrginvrcn  20114  nmoleub  20152  xrsmopn  20231  icccmplem3  20243  reconnlem2  20246  rectbntr0  20251  rescncf  20315  icoopnst  20353  iocopnst  20354  iccpnfcnv  20358  lebnumii  20380  nmoleub2lem  20511  nmhmcn  20517  fgcfil  20624  iscfil3  20626  iscau2  20630  iscau3  20631  iscau4  20632  iscmet3lem2  20645  cfilres  20649  caussi  20650  equivcfil  20652  equivcau  20653  caubl  20660  ivthlem2  20778  ivthlem3  20779  ovoliunlem2  20828  ovoliunnul  20832  ovolicc2lem3  20844  ioombl1lem4  20884  dyadmax  20920  dyadmbl  20922  volsup2  20927  itg2le  21059  itg2const2  21061  itg2seq  21062  itgsplitioo  21157  dvnres  21247  rolle  21304  c1lip1  21311  dvivthlem1  21322  lhop1  21328  dvcnvrelem1  21331  dvfsumrlim  21345  ply1divmo  21492  ig1peu  21528  plypf1  21565  coeaddlem  21601  fta1  21659  quotcan  21660  aalioulem4  21686  ulmcaulem  21744  ulmcn  21749  pilem2  21802  sincosq1lem  21844  sinq12gt0  21854  sinq12ge0  21855  sineq0  21868  tanord1  21878  lognegb  21923  logrec  22100  dcubic  22126  xrlimcnp  22247  o1cxp  22253  ftalem2  22296  ftalem3  22297  fsumdvdscom  22410  chtub  22436  vmasum  22440  bcmono  22501  bposlem3  22510  bposlem7  22514  lgsdir  22554  lgsqrlem2  22566  lgsdchr  22572  lgsquadlem2  22579  2sqlem6  22593  dchrisumlem3  22625  pntrsumbnd2  22701  pntpbnd1  22720  pntibnd  22727  pntlem3  22743  pntleml  22745  brbtwn2  22974  colinearalg  22979  axcontlem10  23042  redwlk  23328  fargshiftf1  23346  constr3trllem2  23360  4cycl4dv  23376  vdusgra0nedg  23401  usgravd0nedg  23405  eupath2  23424  ex-natded5.3-2  23438  isgrpo  23506  opidon  23632  vacn  23912  ubthlem2  24095  htthlem  24142  normgt0  24352  shmodsi  24615  spansneleq  24796  h1datomi  24807  pjjsi  24926  nmcexi  25253  pjnormssi  25395  stm1add3i  25474  golem2  25499  cvnsym  25517  dmdmd  25527  mdslmd1lem1  25552  mdslmd1i  25556  mdexchi  25562  atcveq0  25575  superpos  25581  hatomistici  25589  atoml2i  25610  atcvat2i  25614  chirredlem1  25617  atcvat3i  25623  mdsymlem3  25632  mdsymlem5  25634  cdj3lem2b  25664  cdj3i  25668  supssd  25828  resspos  25943  resstos  25944  submarchi  26027  tpr2rico  26196  ordtrest2NEWlem  26206  xrge0iifcnv  26217  eulerpartlemb  26599  ballotlemfc0  26723  ballotlemfcc  26724  subfacp1lem6  26921  iccllyscon  26987  cvmfolem  27016  cvmliftlem7  27028  cvmliftlem10  27031  ghomf1olem  27160  fprodss  27308  fundmpss  27424  dfon2lem3  27445  dfon2lem6  27448  axext4dist  27461  setlikess  27503  trpredtr  27541  trpredmintr  27542  dftrpred3g  27544  trpredrec  27549  frmin  27550  soseq  27562  wfrlem12  27582  frrlem5e  27623  frrlem11  27627  sltval2  27644  sltres  27652  nodenselem4  27672  nodenselem8  27676  nobndlem6  27685  dfrdg4  27828  5segofs  27884  cgrextend  27886  segconeu  27889  btwncomim  27891  btwnswapid  27895  btwnintr  27897  btwnexch3  27898  btwndiff  27905  ifscgr  27922  cgrxfr  27933  btwnxfr  27934  lineext  27954  brofs2  27955  linecgr  27959  lineid  27961  idinside  27962  endofsegid  27963  btwnconn1lem13  27977  btwnconn3  27981  onsuct0  28135  limsucncmpi  28139  wl-aetr  28207  fin2so  28260  ltflcei  28263  tan2h  28268  heicant  28270  mblfinlem2  28273  mblfinlem3  28274  itg2addnclem  28287  itg2addnclem2  28288  itg2gt0cn  28291  ftc1anclem5  28315  ftc1anclem6  28316  finminlem  28357  nn0prpwlem  28361  cldbnd  28365  clsint2  28368  reftr  28405  fnessref  28409  comppfsc  28423  neibastop3  28427  fgmin  28435  filbcmb  28478  nninfnub  28491  mettrifi  28497  geomcau  28499  istotbnd3  28514  sstotbnd2  28517  ismtybndlem  28549  heibor1lem  28552  heiborlem1  28554  heiborlem8  28561  heiborlem10  28563  heibor  28564  riscer  28638  crngohomfo  28650  keridl  28676  ispridl2  28682  ispridlc  28714  fphpdo  29001  icodiamlt  29006  pellexlem5  29019  pellexlem6  29020  jm2.26lem3  29195  dfac21  29264  unxpwdom3  29293  ordpss  29552  stoweidlem34  29675  ralralimp  29965  ltsubnn0  30028  elfz2z  30044  usg2wlkeq  30135  usgra2adedgspthlem2  30150  wwlknred  30201  wwlknextbi  30203  wwlkm1edg  30213  usg2wotspth  30249  clwlkswlks  30269  clwlkisclwwlklem2fv2  30291  clwlkisclwwlklem2a  30293  clwlkisclwwlklem1  30295  clwwlkf  30302  clwwlkext2edg  30310  wwlksubclwwlk  30312  zm1nn  30314  clwwisshclwwlem1  30315  usgravd00  30384  frgraregorufrg  30511  numclwwlkovf2ex  30525  numclwlk1lem2foa  30530  numclwlk1lem2fo  30534  ztprmneprm  30583  lcosslsp  30681  lindslinindsimp1  30700  lindslinindsimp2lem5  30705  snlindsntor  30714  19.41rg  30960  lsatcveq0  32250  eqlkr3  32319  atlatmstc  32537  atlrelat1  32539  hlrelat2  32620  intnatN  32624  cvrexchlem  32636  cvratlem  32638  cvrat2  32646  atltcvr  32652  cvrat3  32659  cvrat4  32660  ps-1  32694  ps-2  32695  lplnnle2at  32758  lvolnle3at  32799  2llnma3r  33005  cdlemblem  33010  pmapjoin  33069  elpcliN  33110  lhpmcvr4N  33243  4atexlemnclw  33287  trlnidatb  33394  cdlemc4  33411  cdlemd3  33417  cdleme3g  33451  cdleme7d  33463  cdleme11c  33478  cdleme11dN  33479  cdleme21b  33543  cdleme21c  33544  cdleme21i  33552  cdleme22b  33558  cdleme35fnpq  33666  cdlemf1  33778  trlord  33786  cdlemg6c  33837  dihglblem6  34558  dochlkr  34603  dochkrshp  34604  dihjat1lem  34646  dochexmidlem5  34682  dochexmidlem8  34685