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	⊢ (𝜑 → 𝜓)
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  36  syl2im  40  imim12i  62  pm2.86d  108  con2d  134  con3d  152  nsyli  157  biimtrid  241  biimtrrid  242  imbitrid  243  adantld  492  adantrd  493  impel  507  mpan9  508  pm4.72  949  pm2.36  969  pm4.79  1003  ecased  1034  ecase3adOLD  1036  alrimdh  1867  stdpc5v  1942  19.37imv  1952  ax12w  2130  ax13dgen2  2135  ax12v  2173  spsd  2181  nf5r  2188  axc4  2315  equs5eALT  2365  ax13lem1  2374  nfeqf  2381  hbae  2431  ax12vALT  2469  2ax6elem  2470  sb1  2478  euimmo  2613  necon2ad  2956  necon4ad  2960  r19.37v  3182  spcimgft  3578  rr19.28v  3659  moeq3  3709  reuimrmo  3742  sbeqalb  3846  csbexg  5311  ralxfrd  5407  ralxfrd2  5411  ralxfrALT  5414  copsexgw  5491  copsexg  5492  pwssun  5572  somo  5626  ssrel  5783  ssrelOLD  5784  relssres  6023  dmsnopg  6213  dfco2a  6246  dfpo2  6296  frpoinsg  6345  wfisgOLD  6356  tz7.7  6391  ordunidif  6414  suctr  6451  trsucss  6453  suc11  6472  imadif  6633  dffv2  6987  fvmptd3f  7014  fvmptnf  7021  foco2  7109  fconst5  7207  isores3  7332  riotaxfrd  7400  ovmpt4g  7555  ovmpos  7556  ov2gf  7557  ovmpodf  7564  sorpsscmpl  7724  abnexg  7743  onint  7778  limuni3  7841  tfisg  7843  tfis  7844  tfinds  7849  limomss  7860  peano5  7884  peano5OLD  7885  fo2ndf  8107  frxp  8112  xpord2pred  8131  xpord2indlem  8133  soseq  8145  suppss2  8185  suppssfv  8187  rntpos  8224  fprlem1  8285  fprresex  8295  wfr3g  8307  wfrlem5OLD  8313  wfrlem17OLD  8325  onfununi  8341  smofvon2  8356  smo11  8364  smoord  8365  tfrlem11  8388  tz7.44-2  8407  tz7.48lem  8441  tz7.48-1  8443  tz7.49  8445  tz7.49c  8446  omordi  8566  omord  8568  omass  8580  oneo  8581  omeulem1  8582  omopth2  8584  oewordri  8592  oeworde  8593  nnmordi  8631  nnmord  8632  omabs  8650  nnneo  8654  omsmo  8657  naddcllem  8675  qsel  8790  eceqoveq  8816  domunsncan  9072  sucdom2OLD  9082  sbthlem1  9083  2pwuninel  9132  mapen  9141  infensuc  9155  rexdif1en  9158  findcard2  9164  pssnn  9168  ssfi  9173  sucdom2  9206  php  9210  onomeneq  9228  0sdom1dom  9238  sdom1  9242  pssnnOLD  9265  dif1ennnALT  9277  findcard2OLD  9284  ac6sfi  9287  frfi  9288  unblem1  9295  unblem2  9296  unbnn2  9300  nnsdomgOLD  9303  xpfiOLD  9318  domunfican  9320  fiint  9324  ixpfi2  9350  finsschain  9359  marypha1lem  9428  oiexg  9530  brwdom3  9577  inf3lem2  9624  inf3lem3  9625  cantnfval2  9664  cantnflt  9667  cantnflem1  9684  cnfcom  9695  ttrclss  9715  trcl  9723  epfrs  9726  frmin  9744  frinsg  9746  frr3g  9751  frrlem15  9752  r1sdom  9769  cardsdomel  9969  carduni  9976  pr2neOLD  10000  infpwfien  10057  carduniima  10091  dfac5  10123  dfac12r  10141  dfac12k  10142  kmlem11  10155  djuinf  10183  infxp  10210  cfsuc  10252  cfcoflem  10267  coftr  10268  infpssr  10303  fin23lem30  10337  isf32lem1  10348  isf34lem6  10375  fin1a2lem13  10407  fin1a2s  10409  axcc2lem  10431  domtriomlem  10437  axcclem  10452  ac6num  10474  zorn2lem5  10495  zorn2lem6  10496  axdclem2  10515  alephval2  10567  alephreg  10577  pwcfsdom  10578  axregndlem1  10597  axregnd  10599  axacndlem1  10602  axacndlem2  10603  axacndlem3  10604  axacndlem4  10605  axacnd  10607  gchi  10619  fpwwe2lem12  10637  canthp1  10649  gchpwdom  10665  wunfi  10716  tskwe2  10768  inar1  10770  gruen  10807  intgru  10809  indpi  10902  nqereu  10924  ltbtwnnq  10973  prnmadd  10992  genpcd  11001  prlem934  11028  ltexprlem1  11031  ltexprlem2  11032  ltexprlem7  11037  ltaprlem  11039  ltapr  11040  reclem4pr  11045  suplem2pr  11048  mulcmpblnr  11066  recexsrlem  11098  mulgt0sr  11100  supsrlem  11106  axpre-sup  11164  1re  11214  dedekindle  11378  addlsub  11630  recex  11846  nnunb  12468  0mnnnnn0  12504  prime  12643  zeo  12648  fnn0ind  12661  zindd  12663  btwnz  12665  lbzbi  12920  xrub  13291  elfznelfzo  13737  addmodlteq  13911  facwordi  14249  fiinfnf1o  14310  hashclb  14318  hashdom  14339  hashf1lem2  14417  seqcoll  14425  brfi1indALT  14461  ccatalpha  14543  pfxccatin12lem2a  14677  limsupbnd2  15427  rlimdm  15495  o1of2  15557  rlimno1  15600  isercoll  15614  caurcvg2  15624  caucvgb  15626  serf0  15627  zsum  15664  fsum2dlem  15716  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  zprod  15881  fprod2dlem  15924  fprod2d  15925  odd2np1  16284  ndvdssub  16352  dfgcd2  16488  nprm  16625  maxprmfct  16646  rpexp  16659  pc2dvds  16812  pcfac  16832  unbenlem  16841  4sqlem12  16889  4sqlem17  16894  vdwlem13  16926  prmlem0  17039  mreiincl  17540  sscfn1  17764  initoid  17951  termoid  17952  funcestrcsetclem8  18099  funcsetcestrclem8  18114  pospo  18298  cnvpsb  18532  dirtr  18555  mulgaddcom  18978  mulginvcom  18979  gaass  19161  cntz2ss  19199  elsymgbas  19241  symgfix2  19284  pmtrfrn  19326  psgnran  19383  odmulg  19424  odhash3  19444  sylow2alem1  19485  sylow2alem2  19486  pj1eu  19564  efgs1b  19604  efgsfo  19607  efgredlemc  19613  efgredeu  19620  frgpuptinv  19639  lt6abl  19763  ghmcyg  19764  ablfac1eulem  19942  pgpfac1lem5  19949  ablsimpgfindlem1  19977  ringinvnz1ne0  20112  irredmul  20243  acsfn1p  20415  lspextmo  20667  lspsncv0  20759  psgnghm  21133  mplcoe1  21592  mplcoe5  21595  evlseu  21646  mhpsclcl  21690  mdetunilem7  22120  mdetunilem9  22122  chcoeffeq  22388  cnindis  22796  lmss  22802  lmcls  22806  lmcnp  22808  hausnei  22832  cmpsub  22904  tgcmp  22905  fiuncmp  22908  cmpfi  22912  bwth  22914  1stcrest  22957  2ndcdisj  22960  1stccnp  22966  comppfsc  23036  1stckgenlem  23057  txcls  23108  txcn  23130  txlm  23152  tx1stc  23154  xkococn  23164  hmphdis  23300  ptcmpfi  23317  isfild  23362  fgss2  23378  filconn  23387  trfil2  23391  ufileu  23423  filufint  23424  elfm2  23452  flftg  23500  fclssscls  23522  fclscf  23529  ufilcmp  23536  cnpfcf  23545  alexsubb  23550  alexsubALTlem4  23554  alexsubALT  23555  qustgpopn  23624  tsmsxp  23659  isust  23708  xmettri2  23846  blin2  23935  setsmstopn  23986  met2ndc  24032  metcnp3  24049  tngtopn  24167  reconnlem2  24343  xrge0tsms  24350  fsumcn  24386  bndth  24474  iscmet3lem2  24809  iscmet3  24810  ivthlem1  24968  ivthlem2  24969  ivthlem3  24970  ovolfiniun  25018  volfiniun  25064  ioombl1lem4  25078  ismbf3d  25171  mbfi1flimlem  25240  itg2seq  25260  itgfsum  25344  ellimc3  25396  dvmptfsum  25492  c1liplem1  25513  plypf1  25726  plydivex  25810  aannenlem1  25841  ulmval  25892  ulmcau  25907  ulmbdd  25910  ulmcn  25911  ulmdvlem3  25914  sineq0  26033  efopn  26166  cxpeq  26265  logbgcd1irr  26299  rlimcnp  26470  xrlimcnp  26473  lgsdir2lem2  26829  lgsne0  26838  2lgsoddprm  26919  2sqlem6  26926  2sqlem10  26931  2sqreunnltblem  26954  sltval2  27159  noetasuplem4  27239  conway  27300  madebdayim  27382  addsass  27488  axcontlem2  28223  uhgr0vb  28332  uvtx01vtx  28654  uvtxupgrres  28665  fusgrn0degnn0  28756  finsumvtxdg2size  28807  cusgrm1rusgr  28839  wlkv0  28908  wlklenvclwlk  28912  uspgrn2crct  29062  frrusgrord  29594  numclwwlk1lem2fo  29611  isgrpo  29750  grpoidinvlem3  29759  vcdi  29818  vcdir  29819  vcass  29820  nvs  29916  nvtri  29923  blocnilem  30057  chintcli  30584  hsupss  30594  shlej1  30613  elspansn4  30826  spansncvi  30905  hoaddsub  31069  lnopl  31167  lnfnl  31184  riesz4i  31316  pjnormssi  31421  pj3si  31460  stlei  31493  stcltr2i  31528  dmdmd  31553  dmdbr5  31561  mdslmd1lem2  31579  atssma  31631  atcvatlem  31638  chirredlem1  31643  atcvat4i  31650  mdsymlem2  31657  mdsymlem6  31661  sumdmdlem2  31672  cdjreui  31685  elimifd  31775  disjxpin  31819  unifi3  31937  xrge0infss  31973  xrge0tsmsd  32209  gsumle  32242  gsumvsca1  32371  gsumvsca2  32372  lmxrge0  32932  ismeas  33197  eulerpartlemb  33367  bnj849  33936  bnj1110  33993  srcmpltd  34085  swrdrevpfx  34107  cusgredgex2  34113  subgrwlk  34123  cusgr3cyclex  34127  umgr2cycllem  34131  umgr2cycl  34132  connpconn  34226  cvmseu  34267  cvmliftlem15  34289  cvmlift2lem1  34293  cvmlift2lem12  34305  satfv0fun  34362  satffunlem  34392  mclsind  34561  dfon2lem3  34757  dfon2lem4  34758  dfon2lem6  34760  dfon2lem8  34762  dfon2lem9  34763  hbntg  34777  cgrdegen  34976  funtransport  35003  ifscgr  35016  cgrxfr  35027  brofs2  35049  brifs2  35050  idinside  35056  btwnconn1lem7  35065  btwnconn1lem11  35069  btwnconn1lem12  35070  btwnconn1lem14  35072  broutsideof2  35094  btwnoutside  35097  outsideoftr  35101  finminlem  35203  ntruni  35212  neibastop1  35244  ontgval  35316  ordtop  35321  ordcmp  35332  onint1  35334  bj-ax12w  35554  axc11n11r  35561  bj-ax12v3  35563  bj-nnfan  35626  bj-nnfand  35627  bj-nnflemea  35643  bj-19.42t  35651  bj-sbft  35653  bj-hbaeb2  35696  bj-spcimdv  35775  bj-spcimdvv  35776  bj-sngltag  35864  bj-xtagex  35870  bj-0int  35982  bj-ismooredr  35990  bj-inftyexpiinj  36090  nlpfvineqsn  36290  wl-ax13lem1  36375  wl-speqv  36391  wl-sbcom2d  36426  wl-ax11-lem3  36449  wl-ax11-lem8  36454  tan2h  36480  ptrest  36487  poimirlem20  36508  poimirlem22  36510  poimirlem26  36514  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  heicant  36523  voliunnfl  36532  volsupnfl  36533  itg2addnclem2  36540  itg2addnc  36542  itg2gt0cn  36543  ftc2nc  36570  filbcmb  36608  sdclem2  36610  seqpo  36615  nninfnub  36619  neificl  36621  prdstotbnd  36662  cnpwstotbnd  36665  heibor1lem  36677  heibor  36689  bfplem2  36691  opidonOLD  36720  exidu1  36724  grpokerinj  36761  rngoideu  36771  rngodi  36772  rngodir  36773  rngmgmbs4  36799  divrngidl  36896  prnc  36935  eqvrelqsel  37486  erimeq2  37548  prter2  37751  ax4fromc4  37764  hbae-o  37773  dvelimf-o  37799  ax12indn  37813  ax12inda2  37817  ax12a2-o  37820  l1cvpat  37924  atcvrj0  38299  pmaple  38632  paddasslem5  38695  pclfinN  38771  osumcllem11N  38837  pexmidlem8N  38848  dvheveccl  39983  dihord6apre  40127  lpolconN  40358  lcmineqlem1  40894  oexpreposd  41212  sn-it0e0  41288  cnreeu  41341  isnacs3  41448  pellexlem5  41571  pellex  41573  jm2.18  41727  jm2.15nn0  41742  jm2.16nn0  41743  dford3lem2  41766  ttac  41775  onexomgt  41990  onexoegt  41993  omabs2  42082  omcl3g  42084  tfsconcat0b  42096  naddgeoa  42145  safesnsupfiss  42166  rp-isfinite5  42268  cnvssb  42337  clcnvlem  42374  iunrelexpuztr  42470  rfovcnvf1od  42755  ntrrn  42873  nzss  43076  pm11.71  43156  axc11next  43165  hbntal  43314  eel2122old  43479  fsetsnf1  45762  2reu8i  45821  afvelima  45875  rlimdmafv  45885  rlimdmafv2  45966  elsprel  46143  sfprmdvdsmersenne  46271  perfectALTVlem2  46390  fpprwppr  46407  copisnmnd  46579  pzriprnglem12  46816  rnghmsscmap2  46871  rnghmsscmap  46872  rhmsscmap2  46917  rhmsscmap  46918  funcringcsetcALTV2lem8  46941  funcringcsetclem8ALTV  46964  lindslinindsimp2lem5  47143  nn0sumshdig  47309  prelrrx2b  47400  itscnhlc0yqe  47445  iscnrm3lem2  47567  spd  47723  setrec1lem4  47735  setrec2fun  47737  aacllem  47848