Theorem syl5 33

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	⊢ (𝜑 → 𝜓)
syl5.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5com 31	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  35  syl2im  39  imim12i  60  peirceroll  83  pm2.86d  105  con2d  128  con3d  147  nsyli  154  syl5bi  231  syl5bir  232  syl5ib  233  adantld  482  adantrd  483  impel  484  mpan9  485  pm4.79  605  pm2.36  884  pm4.72  916  ecased  982  ecase3ad  983  syl3an2  1352  syl2an23an  1379  alrimdh  1777  stdpc5v  1854  ax12w  1997  ax13dgen2  2002  ax12v  2035  ax12vOLD  2037  ax12vOLDOLD  2038  spsd  2045  nf5r  2052  axc4  2115  equs5eALT  2166  ax13lem1  2236  nfeqf  2289  hbae  2303  ax12vALT  2416  2ax6elem  2437  euimmo  2510  necon2ad  2797  necon4ad  2801  spcimgft  3257  rr19.28v  3315  moeq3  3350  sbeqalb  3455  csbexg  4720  reusv2lem2OLD  4796  ralxfrd  4805  ralxfrdOLD  4806  ralxfrd2  4810  ralxfrALT  4813  copsexg  4882  pwssun  4944  somo  4993  ssrel  5130  relssres  5357  issref  5428  dmsnopg  5524  dfco2a  5552  wfisg  5632  tz7.7  5666  ordunidif  5690  suctr  5725  trsucss  5728  suc11  5748  imadif  5887  fvelima  6158  dffv2  6181  fvmptdf  6204  fvmptf  6209  fvmptnf  6210  foco2  6287  foco2OLD  6288  fconst5  6376  funfvima2  6397  funfvima3  6399  isores3  6485  riotaxfrd  6541  oprabid  6576  ovmpt4g  6681  ovmpt2s  6682  ov2gf  6683  ovmpt2df  6690  sorpsscmpl  6846  onint  6887  limuni3  6944  tfi  6945  tfis  6946  tfinds  6951  limomss  6962  peano5  6981  fo2ndf  7171  frxp  7174  suppssov1  7214  suppss2  7216  suppssfv  7218  rntpos  7252  tposf2  7263  wfr3g  7300  wfrlem4  7305  wfrlem5  7306  wfrlem17  7318  onfununi  7325  smofvon2  7340  smo11  7348  smoord  7349  tfrlem11  7371  tz7.44-2  7390  tz7.48lem  7423  tz7.48-1  7425  tz7.49  7427  tz7.49c  7428  omordi  7533  omord  7535  omass  7547  oneo  7548  omeulem1  7549  omopth2  7551  oewordri  7559  oeworde  7560  nnmordi  7598  nnmord  7599  omabs  7614  nnneo  7618  omsmo  7621  ectocld  7701  qsel  7713  eceqoveq  7740  mapsn  7785  f1oeng  7860  domunsncan  7945  sbthlem1  7955  2pwuninel  8000  mapen  8009  infensuc  8023  nneneq  8028  sucdom2  8041  pssnn  8063  dif1en  8078  findcard2  8085  ac6sfi  8089  frfi  8090  unblem1  8097  unblem2  8098  unbnn2  8102  nnsdomg  8104  xpfi  8116  domunfican  8118  fiint  8122  fodomfi  8124  ixpfi2  8147  finsschain  8156  marypha1lem  8222  oiexg  8323  brwdom3  8370  inf3lem2  8409  inf3lem3  8410  cantnfval2  8449  cantnflt  8452  cantnflem1  8469  cantnf  8473  cnfcom  8480  trcl  8487  epfrs  8490  r1sdom  8520  rankwflemb  8539  rankelb  8570  carden2a  8675  cardsdomel  8683  carduni  8690  harval2  8706  pr2ne  8711  infpwfien  8768  cardaleph  8795  carduniima  8802  alephval3  8816  dfac5  8834  dfac12r  8851  dfac12k  8852  kmlem4  8858  kmlem11  8865  kmlem12  8866  cdainf  8897  infxp  8920  cfsuc  8962  cfcoflem  8977  coftr  8978  cfcof  8979  infpssr  9013  fin23lem30  9047  isf32lem1  9058  isf34lem6  9085  fin1a2lem13  9117  fin1a2s  9119  axcc2lem  9141  domtriomlem  9147  axdc4lem  9160  axcclem  9162  ac6num  9184  zorn2lem5  9205  zorn2lem6  9206  axdclem2  9225  alephval2  9273  alephreg  9283  pwcfsdom  9284  axregndlem1  9303  axregnd  9305  axacndlem1  9308  axacndlem2  9309  axacndlem3  9310  axacndlem4  9311  axacnd  9313  gchi  9325  fpwwe2lem13  9343  canthp1  9355  gchpwdom  9371  wunfi  9422  tskwe2  9474  inar1  9476  gruen  9513  intgru  9515  indpi  9608  nqereu  9630  ltbtwnnq  9679  prnmadd  9698  genpcd  9707  prlem934  9734  ltexprlem1  9737  ltexprlem2  9738  ltexprlem7  9743  ltaprlem  9745  ltapr  9746  reclem4pr  9751  suplem2pr  9754  mulcmpblnr  9771  recexsrlem  9803  mulgt0sr  9805  recexsr  9807  supsrlem  9811  axpre-sup  9869  1re  9918  dedekindle  10080  addlsub  10326  recex  10538  nnunb  11165  0mnnnnn0  11202  prime  11334  zeo  11339  fnn0ind  11352  zindd  11354  btwnz  11355  lbzbi  11652  xrub  12014  elfznelfzo  12439  addmodlteq  12607  facwordi  12938  fiinfnf1o  13000  hashclb  13011  hashdom  13029  hashf1lem2  13097  seqcoll  13105  hash2pwpr  13115  brfi1indALT  13137  brfi1indALTOLD  13143  ccatalpha  13228  swrdccatin12lem2a  13336  limsupbnd2  14062  rlimdm  14130  o1of2  14191  rlimno1  14232  isercoll  14246  climcau  14249  caurcvg2  14256  caucvgb  14258  serf0  14259  zsum  14296  fsum2dlem  14343  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  zprod  14506  fprod2dlem  14549  fprod2d  14550  odd2np1  14903  ndvdssub  14971  dfgcd2  15101  coprmproddvdslem  15214  nprm  15239  maxprmfct  15259  rpexp  15270  pc2dvds  15421  pcfac  15441  unbenlem  15450  4sqlem12  15498  4sqlem17  15503  vdwlem6  15528  vdwlem13  15535  prmlem0  15650  xpscfv  16045  mreiincl  16079  sscfn1  16300  initoid  16478  termoid  16479  funcestrcsetclem8  16610  funcsetcestrclem8  16625  pospo  16796  cnvpsb  17036  dirref  17058  dirtr  17059  mulgaddcom  17387  mulginvcom  17388  gaass  17553  cntz2ss  17588  elsymgbas  17625  symgfix2  17659  pmtrfrn  17701  psgnran  17758  odmulg  17796  odhash3  17814  sylow2alem1  17855  sylow2alem2  17856  pj1eu  17932  efgs1b  17972  efgsfo  17975  efgredlemc  17981  efgredeu  17988  frgpuptinv  18007  lt6abl  18119  ghmcyg  18120  ablfac1eulem  18294  pgpfac1lem5  18301  ringinvnz1ne0  18415  irredn1  18529  irredmul  18532  lspextmo  18877  lspsncv0  18967  mplcoe1  19286  mplcoe5  19289  evlseu  19337  psgnghm  19745  mdetunilem7  20243  mdetunilem9  20245  chcoeffeq  20510  cnindis  20906  lmss  20912  lmcls  20916  lmcnp  20918  hausnei  20942  cmpsub  21013  tgcmp  21014  fiuncmp  21017  cmpfi  21021  bwth  21023  1stcrest  21066  2ndcdisj  21069  1stccnp  21075  comppfsc  21145  1stckgenlem  21166  txcls  21217  txcn  21239  txlm  21261  tx1stc  21263  xkococn  21273  hmphdis  21409  ptcmpfi  21426  isfild  21472  fgss2  21488  filcon  21497  trfil2  21501  ufileu  21533  filufint  21534  elfm2  21562  flftg  21610  cnpflf2  21614  fclssscls  21632  fclscf  21639  ufilcmp  21646  cnpfcf  21655  alexsubb  21660  alexsubALTlem4  21664  alexsubALT  21665  cnextcn  21681  qustgpopn  21733  tsmsxp  21768  isust  21817  xmettri2  21955  blin2  22044  setsmstopn  22093  met2ndc  22138  metcnp3  22155  tngtopn  22264  reconnlem2  22438  xrge0tsms  22445  fsumcn  22481  bndth  22565  iscmet3lem2  22898  iscmet3  22899  ivthlem1  23027  ivthlem2  23028  ivthlem3  23029  ovolfiniun  23076  volfiniun  23122  ioombl1lem4  23136  dyadmbl  23174  ismbf3d  23227  itg1addlem4  23272  mbfi1flimlem  23295  itg2seq  23315  itgfsum  23399  ellimc3  23449  dvmptfsum  23542  c1liplem1  23563  plypf1  23772  plydivex  23856  aannenlem1  23887  ulmval  23938  ulmcau  23953  ulmss  23955  ulmbdd  23956  ulmcn  23957  ulmdvlem3  23960  pserulm  23980  sineq0  24077  efopn  24204  cxpeq  24298  rlimcnp  24492  xrlimcnp  24495  perfectlem2  24755  lgsdir2lem2  24851  lgsne0  24860  2lgsoddprm  24941  2sqlem6  24948  2sqlem10  24953  dchrisumlem2  24979  axlowdimlem16  25637  axcontlem2  25645  uhgr0vb  25738  usgrcyclnl1  26168  4cycl4dv  26195  el2wlkonot  26396  2wlkonot3v  26402  2spthonot3v  26403  cusgraiffrusgra  26467  2pthfrgra  26538  isgrpo  26735  grpoidinvlem3  26744  vcdi  26804  vcdir  26805  vcass  26806  nvs  26902  nvtri  26909  blocnilem  27043  chintcli  27574  hsupss  27584  shlej1  27603  elspansn4  27816  spansncvi  27895  hoaddsub  28059  lnopl  28157  lnfnl  28174  riesz4i  28306  pjnormssi  28411  pj3si  28450  stlei  28483  stcltr2i  28518  dmdmd  28543  dmdbr5  28551  mdslmd1lem2  28569  atssma  28621  atcvatlem  28628  chirredlem1  28633  atcvat4i  28640  mdsymlem2  28647  mdsymlem6  28651  sumdmdlem2  28662  dmdbr5ati  28665  cdjreui  28675  elimifd  28746  disjxpin  28783  unifi3  28873  xrge0infss  28915  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  xrge0tsmsd  29116  lmxrge0  29326  ismeas  29589  eulerpartlemb  29757  bnj849  30249  bnj1110  30304  conpcon  30471  cvmseu  30512  cvmliftlem15  30534  cvmlift2lem1  30538  cvmlift2lem12  30550  mclsind  30721  dfpo2  30898  fundmpss  30910  dfon2lem3  30934  dfon2lem4  30935  dfon2lem6  30937  dfon2lem8  30939  dfon2lem9  30940  hbntg  30955  tfisg  30960  dftrpred3g  30977  trpredrec  30982  frinsg  30986  soseq  30995  frr3g  31023  frrlem4  31027  frrlem5  31028  sltval2  31053  nodenselem5  31084  cgrdegen  31281  funtransport  31308  ifscgr  31321  cgrxfr  31332  brofs2  31354  brifs2  31355  idinside  31361  btwnconn1lem7  31370  btwnconn1lem11  31374  btwnconn1lem12  31375  btwnconn1lem14  31377  broutsideof2  31399  btwnoutside  31402  outsideoftr  31406  finminlem  31482  ntruni  31492  neibastop1  31524  ontgval  31600  ordtop  31605  ordcmp  31616  onint1  31618  bj-ax12w  31852  axc11n11r  31860  bj-ax12v3  31862  bj-hbaeb2  31993  bj-spcimdv  32078  bj-sngltag  32164  bj-xtagex  32170  bj-inftyexpiinj  32273  wl-ax13lem1  32466  wl-speqv  32487  wl-sbcom2d  32523  wl-ax11-lem3  32543  wl-ax11-lem8  32548  tan2h  32571  ptrest  32578  ptrecube  32579  poimirlem20  32599  poimirlem22  32601  poimirlem26  32605  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  heicant  32614  voliunnfl  32623  volsupnfl  32624  itg2addnclem2  32632  itg2addnc  32634  itg2gt0cn  32635  ftc2nc  32664  filbcmb  32705  sdclem2  32708  seqpo  32713  nninfnub  32717  neificl  32719  prdstotbnd  32763  cnpwstotbnd  32766  heibor1lem  32778  heibor  32790  bfplem2  32792  opidonOLD  32821  exidu1  32825  grpokerinj  32862  rngoideu  32872  rngodi  32873  rngodir  32874  rngmgmbs4  32900  divrngidl  32997  prnc  33036  prter2  33184  ax4fromc4  33197  hbae-o  33206  dvelimf-o  33232  ax12indn  33246  ax12inda2  33250  ax12a2-o  33253  l1cvpat  33359  atcvrj0  33732  pmaple  34065  paddasslem5  34128  pclfinN  34204  osumcllem11N  34270  pexmidlem8N  34281  dvheveccl  35419  dihord6apre  35563  lpolconN  35794  isnacs3  36291  pellexlem5  36415  pellex  36417  jm2.18  36573  jm2.15nn0  36588  jm2.16nn0  36589  dford3lem2  36612  ttac  36621  acsfn1p  36788  rp-isfinite5  36882  cnvssb  36911  clcnvlem  36949  iunrelexpuztr  37030  rfovcnvf1od  37318  ntrrn  37440  nzss  37538  pm11.71  37619  axc11next  37629  hbntal  37790  eel2122old  37964  mapsnd  38383  reuimrmo  39827  afvelima  39896  rlimdmafv  39906  sfprmdvdsmersenne  40058  perfectALTVlem2  40165  uvtxa01vtx0  40623  uvtxupgrres  40635  fusgrn0degnn0  40714  cusgrm1rusgr  40782  1wlkv0  40859  uspgrn2crct  41011  copisnmnd  41599  rnghmsscmap2  41765  rnghmsscmap  41766  rhmsscmap2  41811  rhmsscmap  41812  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  lindslinindsimp2lem5  42045  nn0sumshdig  42215  spd  42223  setrec1lem4  42236  setrec2fun  42238  aacllem  42356