Theorem syl5 34

Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

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

Assertion

Ref	Expression
syl5	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 |- ( ph -> ps )
2		syl5.2	. . 3 |- ( ch -> ( ps -> th ) )
3	1, 2	syl5com 31	. 2 |- ( ph -> ( ch -> th ) )
4	3	com12 32	1 |- ( ch -> ( ph -> 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:  syl56  36  syl2im  40  imim12i  62  peirceroll  85  pm2.86d  107  con2d  129  con3d  148  nsyli  155  syl5bi  232  syl5bir  233  syl5ib  234  adantld  483  adantrd  484  impel  485  mpan9  486  pm4.79  607  pm2.36  888  pm4.72  920  ecased  985  ecase3ad  986  syl3an2  1360  syl2an23an  1387  19.38a  1767  19.38b  1768  alrimdh  1790  stdpc5v  1867  ax12w  2010  ax13dgen2  2015  ax12v  2048  ax12vOLD  2050  ax12vOLDOLD  2051  spsd  2057  nf5r  2064  axc4  2130  equs5eALT  2178  ax13lem1  2248  nfeqf  2301  hbae  2315  ax12vALT  2428  2ax6elem  2449  euimmo  2522  necon2ad  2809  necon4ad  2813  spcimgft  3284  rr19.28v  3346  moeq3  3383  sbeqalb  3488  csbexg  4792  reusv2lem2OLD  4870  ralxfrd  4879  ralxfrdOLD  4880  ralxfrd2  4884  ralxfrALT  4887  copsexg  4956  pwssun  5020  somo  5069  ssrel  5207  relssres  5437  issref  5509  dmsnopg  5606  dfco2a  5635  wfisg  5715  tz7.7  5749  ordunidif  5773  suctr  5808  trsucss  5811  suc11  5831  imadif  5973  fvelima  6248  dffv2  6271  fvmptd3f  6295  fvmptf  6301  fvmptnf  6302  foco2  6379  foco2OLD  6380  fconst5  6471  funfvima2  6493  funfvima3  6495  isores3  6585  riotaxfrd  6642  ovmpt4g  6783  ovmpt2s  6784  ov2gf  6785  ovmpt2df  6792  sorpsscmpl  6948  abnexg  6964  onint  6995  limuni3  7052  tfi  7053  tfis  7054  tfinds  7059  limomss  7070  peano5  7089  fo2ndf  7284  frxp  7287  suppssov1  7327  suppss2  7329  suppssfv  7331  rntpos  7365  tposf2  7376  wfr3g  7413  wfrlem4  7418  wfrlem5  7419  wfrlem17  7431  onfununi  7438  smofvon2  7453  smo11  7461  smoord  7462  tfrlem11  7484  tz7.44-2  7503  tz7.48lem  7536  tz7.48-1  7538  tz7.49  7540  tz7.49c  7541  omordi  7646  omord  7648  omass  7660  oneo  7661  omeulem1  7662  omopth2  7664  oewordri  7672  oeworde  7673  nnmordi  7711  nnmord  7712  omabs  7727  nnneo  7731  omsmo  7734  qsel  7826  eceqoveq  7853  mapsn  7899  f1oeng  7974  domunsncan  8060  sbthlem1  8070  2pwuninel  8115  mapen  8124  infensuc  8138  nneneq  8143  sucdom2  8156  pssnn  8178  dif1en  8193  findcard2  8200  ac6sfi  8204  frfi  8205  unblem1  8212  unblem2  8213  unbnn2  8217  nnsdomg  8219  xpfi  8231  domunfican  8233  fiint  8237  fodomfi  8239  ixpfi2  8264  finsschain  8273  marypha1lem  8339  oiexg  8440  brwdom3  8487  inf3lem2  8526  inf3lem3  8527  cantnfval2  8566  cantnflt  8569  cantnflem1  8586  cantnf  8590  cnfcom  8597  trcl  8604  epfrs  8607  r1sdom  8637  rankwflemb  8656  rankelb  8687  carden2a  8792  cardsdomel  8800  carduni  8807  harval2  8823  pr2ne  8828  infpwfien  8885  cardaleph  8912  carduniima  8919  alephval3  8933  dfac5  8951  dfac12r  8968  dfac12k  8969  kmlem11  8982  cdainf  9014  infxp  9037  cfsuc  9079  cfcoflem  9094  coftr  9095  cfcof  9096  infpssr  9130  fin23lem30  9164  isf32lem1  9175  isf34lem6  9202  fin1a2lem13  9234  fin1a2s  9236  axcc2lem  9258  domtriomlem  9264  axdc4lem  9277  axcclem  9279  ac6num  9301  zorn2lem5  9322  zorn2lem6  9323  axdclem2  9342  alephval2  9394  alephreg  9404  pwcfsdom  9405  axregndlem1  9424  axregnd  9426  axacndlem1  9429  axacndlem2  9430  axacndlem3  9431  axacndlem4  9432  axacnd  9434  gchi  9446  fpwwe2lem13  9464  canthp1  9476  gchpwdom  9492  wunfi  9543  tskwe2  9595  inar1  9597  gruen  9634  intgru  9636  indpi  9729  nqereu  9751  ltbtwnnq  9800  prnmadd  9819  genpcd  9828  prlem934  9855  ltexprlem1  9858  ltexprlem2  9859  ltexprlem7  9864  ltaprlem  9866  ltapr  9867  reclem4pr  9872  suplem2pr  9875  mulcmpblnr  9892  recexsrlem  9924  mulgt0sr  9926  recexsr  9928  supsrlem  9932  axpre-sup  9990  1re  10039  dedekindle  10201  addlsub  10447  recex  10659  nnunb  11288  0mnnnnn0  11325  prime  11458  zeo  11463  fnn0ind  11476  zindd  11478  btwnz  11479  lbzbi  11776  xrub  12142  elfznelfzo  12573  addmodlteq  12745  facwordi  13076  fiinfnf1o  13138  hashclb  13149  hashdom  13168  hashf1lem2  13240  seqcoll  13248  brfi1indALT  13282  brfi1indALTOLD  13288  ccatalpha  13375  swrdccatin12lem2a  13485  limsupbnd2  14214  rlimdm  14282  o1of2  14343  rlimno1  14384  isercoll  14398  climcau  14401  caurcvg2  14408  caucvgb  14410  serf0  14411  zsum  14449  fsum2dlem  14501  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  zprod  14667  fprod2dlem  14710  fprod2d  14711  odd2np1  15065  ndvdssub  15133  dfgcd2  15263  coprmproddvdslem  15376  nprm  15401  maxprmfct  15421  rpexp  15432  pc2dvds  15583  pcfac  15603  unbenlem  15612  4sqlem12  15660  4sqlem17  15665  vdwlem6  15690  vdwlem13  15697  prmlem0  15812  xpscfv  16222  mreiincl  16256  sscfn1  16477  initoid  16655  termoid  16656  funcestrcsetclem8  16787  funcsetcestrclem8  16802  pospo  16973  cnvpsb  17213  dirref  17235  dirtr  17236  mulgaddcom  17564  mulginvcom  17565  gaass  17730  cntz2ss  17765  elsymgbas  17802  symgfix2  17836  pmtrfrn  17878  psgnran  17935  odmulg  17973  odhash3  17991  sylow2alem1  18032  sylow2alem2  18033  pj1eu  18109  efgs1b  18149  efgsfo  18152  efgredlemc  18158  efgredeu  18165  frgpuptinv  18184  lt6abl  18296  ghmcyg  18297  ablfac1eulem  18471  pgpfac1lem5  18478  ringinvnz1ne0  18592  irredn1  18706  irredmul  18709  lspextmo  19056  lspsncv0  19146  mplcoe1  19465  mplcoe5  19468  evlseu  19516  psgnghm  19926  mdetunilem7  20424  mdetunilem9  20426  chcoeffeq  20691  cnindis  21096  lmss  21102  lmcls  21106  lmcnp  21108  hausnei  21132  cmpsub  21203  tgcmp  21204  fiuncmp  21207  cmpfi  21211  bwth  21213  1stcrest  21256  2ndcdisj  21259  1stccnp  21265  comppfsc  21335  1stckgenlem  21356  txcls  21407  txcn  21429  txlm  21451  tx1stc  21453  xkococn  21463  hmphdis  21599  ptcmpfi  21616  isfild  21662  fgss2  21678  filconn  21687  trfil2  21691  ufileu  21723  filufint  21724  elfm2  21752  flftg  21800  fclssscls  21822  fclscf  21829  ufilcmp  21836  cnpfcf  21845  alexsubb  21850  alexsubALTlem4  21854  alexsubALT  21855  cnextcn  21871  qustgpopn  21923  tsmsxp  21958  isust  22007  xmettri2  22145  blin2  22234  setsmstopn  22283  met2ndc  22328  metcnp3  22345  tngtopn  22454  reconnlem2  22630  xrge0tsms  22637  fsumcn  22673  bndth  22757  iscmet3lem2  23090  iscmet3  23091  ivthlem1  23220  ivthlem2  23221  ivthlem3  23222  ovolfiniun  23269  volfiniun  23315  ioombl1lem4  23329  dyadmbl  23368  ismbf3d  23421  itg1addlem4  23466  mbfi1flimlem  23489  itg2seq  23509  itgfsum  23593  ellimc3  23643  dvmptfsum  23738  c1liplem1  23759  plypf1  23968  plydivex  24052  aannenlem1  24083  ulmval  24134  ulmcau  24149  ulmss  24151  ulmbdd  24152  ulmcn  24153  ulmdvlem3  24156  pserulm  24176  sineq0  24273  efopn  24404  cxpeq  24498  rlimcnp  24692  xrlimcnp  24695  perfectlem2  24955  lgsdir2lem2  25051  lgsne0  25060  2lgsoddprm  25141  2sqlem6  25148  2sqlem10  25153  dchrisumlem2  25179  axlowdimlem16  25837  axcontlem2  25845  uhgr0vb  25967  uvtxa01vtx0  26297  uvtxupgrres  26309  fusgrn0degnn0  26395  finsumvtxdg2size  26446  cusgrm1rusgr  26478  wlkv0  26547  uspgrn2crct  26700  frrusgrord  27205  isgrpo  27351  grpoidinvlem3  27360  vcdi  27420  vcdir  27421  vcass  27422  nvs  27518  nvtri  27525  blocnilem  27659  chintcli  28190  hsupss  28200  shlej1  28219  elspansn4  28432  spansncvi  28511  hoaddsub  28675  lnopl  28773  lnfnl  28790  riesz4i  28922  pjnormssi  29027  pj3si  29066  stlei  29099  stcltr2i  29134  dmdmd  29159  dmdbr5  29167  mdslmd1lem2  29185  atssma  29237  atcvatlem  29244  chirredlem1  29249  atcvat4i  29256  mdsymlem2  29263  mdsymlem6  29267  sumdmdlem2  29278  cdjreui  29291  elimifd  29362  disjxpin  29401  unifi3  29490  xrge0infss  29525  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  xrge0tsmsd  29785  lmxrge0  29998  ismeas  30262  eulerpartlemb  30430  bnj849  30995  bnj1110  31050  connpconn  31217  cvmseu  31258  cvmliftlem15  31280  cvmlift2lem1  31284  cvmlift2lem12  31296  mclsind  31467  dfpo2  31645  fundmpss  31664  dfon2lem3  31690  dfon2lem4  31691  dfon2lem6  31693  dfon2lem8  31695  dfon2lem9  31696  hbntg  31711  tfisg  31716  dftrpred3g  31733  trpredrec  31738  frinsg  31742  soseq  31751  frr3g  31779  frrlem4  31783  frrlem5  31784  sltval2  31809  noetalem3  31865  conway  31910  cgrdegen  32111  funtransport  32138  ifscgr  32151  cgrxfr  32162  brofs2  32184  brifs2  32185  idinside  32191  btwnconn1lem7  32200  btwnconn1lem11  32204  btwnconn1lem12  32205  btwnconn1lem14  32207  broutsideof2  32229  btwnoutside  32232  outsideoftr  32236  finminlem  32312  ntruni  32322  neibastop1  32354  ontgval  32430  ordtop  32435  ordcmp  32446  onint1  32448  bj-ax12w  32665  axc11n11r  32673  bj-ax12v3  32675  bj-hbaeb2  32805  bj-spcimdv  32884  bj-spcimdvv  32885  bj-sngltag  32971  bj-xtagex  32977  bj-0int  33055  bj-ismooredr  33064  bj-inftyexpiinj  33096  wl-ax13lem1  33287  wl-speqv  33308  wl-sbcom2d  33344  wl-ax11-lem3  33364  wl-ax11-lem8  33369  tan2h  33401  ptrest  33408  poimirlem20  33429  poimirlem22  33431  poimirlem26  33435  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  heicant  33444  voliunnfl  33453  volsupnfl  33454  itg2addnclem2  33462  itg2addnc  33464  itg2gt0cn  33465  ftc2nc  33494  filbcmb  33535  sdclem2  33538  seqpo  33543  nninfnub  33547  neificl  33549  prdstotbnd  33593  cnpwstotbnd  33596  heibor1lem  33608  heibor  33620  bfplem2  33622  opidonOLD  33651  exidu1  33655  grpokerinj  33692  rngoideu  33702  rngodi  33703  rngodir  33704  rngmgmbs4  33730  divrngidl  33827  prnc  33866  prter2  34166  ax4fromc4  34179  hbae-o  34188  dvelimf-o  34214  ax12indn  34228  ax12inda2  34232  ax12a2-o  34235  l1cvpat  34341  atcvrj0  34714  pmaple  35047  paddasslem5  35110  pclfinN  35186  osumcllem11N  35252  pexmidlem8N  35263  dvheveccl  36401  dihord6apre  36545  lpolconN  36776  isnacs3  37273  pellexlem5  37397  pellex  37399  jm2.18  37555  jm2.15nn0  37570  jm2.16nn0  37571  dford3lem2  37594  ttac  37603  acsfn1p  37769  rp-isfinite5  37863  cnvssb  37892  clcnvlem  37930  iunrelexpuztr  38011  rfovcnvf1od  38298  ntrrn  38420  nzss  38516  pm11.71  38597  axc11next  38607  hbntal  38769  eel2122old  38943  mapsnd  39388  reuimrmo  41178  afvelima  41247  rlimdmafv  41257  sfprmdvdsmersenne  41520  perfectALTVlem2  41631  elsprel  41725  copisnmnd  41809  rnghmsscmap2  41973  rnghmsscmap  41974  rhmsscmap2  42019  rhmsscmap  42020  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  lindslinindsimp2lem5  42251  nn0sumshdig  42417  spd  42425  setrec1lem4  42437  setrec2fun  42439  aacllem  42547