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  242  biimtrrid  243  imbitrid  244  adantld  490  adantrd  491  impel  505  mpan9  506  pm4.72  951  pm2.36  971  pm4.79  1005  ecased  1035  alrimdh  1860  stdpc5v  1935  19.37imv  1944  ax12w  2130  ax13dgen2  2135  ax12v  2175  spsd  2184  nf5r  2191  axc4  2319  equs5eALT  2367  ax13lem1  2376  nfeqf  2383  hbae  2433  ax12vALT  2471  2ax6elem  2472  sb1  2480  euimmo  2613  necon2ad  2952  necon4ad  2956  r19.37v  3179  spcimgfi1OLD  3547  rr19.28v  3667  moeq3  3720  reuimrmo  3753  sbeqalb  3858  csbexg  5315  ralxfrd  5413  ralxfrd2  5417  ralxfrALT  5420  copsexgw  5500  copsexg  5501  pwssun  5579  somo  5634  ssrel  5794  ssrelOLD  5795  relssres  6041  dmsnopg  6234  dfco2a  6267  dfpo2  6317  frpoinsg  6365  wfisgOLD  6376  tz7.7  6411  ordunidif  6434  suctr  6471  trsucss  6473  suc11  6492  imadif  6651  dffv2  7003  fvmptd3f  7030  fvmptnf  7037  foco2  7128  fconst5  7225  fvf1pr  7326  isores3  7354  riotaxfrd  7421  ovmpt4g  7579  ovmpos  7580  ov2gf  7581  ovmpodf  7588  sorpsscmpl  7752  abnexg  7774  onint  7809  limuni3  7872  tfisg  7874  tfis  7875  tfinds  7880  limomss  7891  peano5  7915  fo2ndf  8144  frxp  8149  xpord2pred  8168  xpord2indlem  8170  soseq  8182  suppss2  8223  suppssfv  8225  rntpos  8262  fprlem1  8323  fprresex  8333  wfr3g  8345  wfrlem5OLD  8351  wfrlem17OLD  8363  onfununi  8379  smofvon2  8394  smo11  8402  smoord  8403  tfrlem11  8426  tz7.44-2  8445  tz7.48lem  8479  tz7.48-1  8481  tz7.49  8483  tz7.49c  8484  omordi  8602  omord  8604  omass  8616  oneo  8617  omeulem1  8618  omopth2  8620  oewordri  8628  oeworde  8629  nnmordi  8667  nnmord  8668  omabs  8687  nnneo  8691  omsmo  8694  naddcllem  8712  qsel  8834  eceqoveq  8860  domunsncan  9110  sucdom2OLD  9120  sbthlem1  9121  2pwuninel  9170  mapen  9179  infensuc  9193  rexdif1en  9196  findcard2  9202  pssnn  9206  ssfi  9211  sucdom2  9240  php  9244  onomeneq  9262  0sdom1dom  9271  sdom1  9275  dif1ennnALT  9308  ac6sfi  9317  frfi  9318  unblem1  9325  unblem2  9326  unbnn2  9330  nnsdomgOLD  9333  xpfiOLD  9356  domunfican  9358  fiintOLD  9364  fodomfir  9365  ixpfi2  9387  finsschain  9396  marypha1lem  9470  oiexg  9572  brwdom3  9619  inf3lem2  9666  inf3lem3  9667  cantnfval2  9706  cantnflt  9709  cantnflem1  9726  cnfcom  9737  ttrclss  9757  trcl  9765  epfrs  9768  frmin  9786  frinsg  9788  frr3g  9793  frrlem15  9794  r1sdom  9811  cardsdomel  10011  carduni  10018  pr2neOLD  10042  infpwfien  10099  carduniima  10133  dfac5  10166  dfac12r  10184  dfac12k  10185  kmlem11  10198  djuinf  10226  infxp  10251  cfsuc  10294  cfcoflem  10309  coftr  10310  infpssr  10345  fin23lem30  10379  isf32lem1  10390  isf34lem6  10417  fin1a2lem13  10449  fin1a2s  10451  axcc2lem  10473  domtriomlem  10479  axcclem  10494  ac6num  10516  zorn2lem5  10537  zorn2lem6  10538  axdclem2  10557  alephval2  10609  alephreg  10619  pwcfsdom  10620  axregndlem1  10639  axregnd  10641  axacndlem1  10644  axacndlem2  10645  axacndlem3  10646  axacndlem4  10647  axacnd  10649  gchi  10661  fpwwe2lem12  10679  canthp1  10691  gchpwdom  10707  wunfi  10758  tskwe2  10810  inar1  10812  gruen  10849  intgru  10851  indpi  10944  nqereu  10966  ltbtwnnq  11015  prnmadd  11034  genpcd  11043  prlem934  11070  ltexprlem1  11073  ltexprlem2  11074  ltexprlem7  11079  ltaprlem  11081  ltapr  11082  reclem4pr  11087  suplem2pr  11090  mulcmpblnr  11108  recexsrlem  11140  mulgt0sr  11142  supsrlem  11148  axpre-sup  11206  1re  11258  dedekindle  11422  addlsub  11676  recex  11892  nnunb  12519  0mnnnnn0  12555  prime  12696  zeo  12701  fnn0ind  12714  zindd  12716  btwnz  12718  lbzbi  12975  xrub  13350  elfznelfzo  13807  fvf1tp  13825  addmodlteq  13983  facwordi  14324  fiinfnf1o  14385  hashclb  14393  hashdom  14414  hashf1lem2  14491  seqcoll  14499  brfi1indALT  14545  ccatalpha  14627  pfxccatin12lem2a  14761  limsupbnd2  15515  rlimdm  15583  o1of2  15645  rlimno1  15686  isercoll  15700  caurcvg2  15710  caucvgb  15712  serf0  15713  zsum  15750  fsum2dlem  15802  fsum2d  15803  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  zprod  15969  fprod2dlem  16012  fprod2d  16013  odd2np1  16374  ndvdssub  16442  dfgcd2  16579  nprm  16721  maxprmfct  16742  rpexp  16755  pc2dvds  16912  pcfac  16932  unbenlem  16941  4sqlem12  16989  4sqlem17  16994  vdwlem13  17026  prmlem0  17139  mreiincl  17640  sscfn1  17864  initoid  18054  termoid  18055  funcestrcsetclem8  18202  funcsetcestrclem8  18217  pospo  18402  cnvpsb  18636  dirtr  18659  mulgaddcom  19128  mulginvcom  19129  gaass  19327  cntz2ss  19365  elsymgbas  19405  symgfix2  19448  pmtrfrn  19490  psgnran  19547  odmulg  19588  odhash3  19608  sylow2alem1  19649  sylow2alem2  19650  pj1eu  19728  efgs1b  19768  efgsfo  19771  efgredlemc  19777  efgredeu  19784  frgpuptinv  19803  lt6abl  19927  ghmcyg  19928  ablfac1eulem  20106  pgpfac1lem5  20113  ablsimpgfindlem1  20141  ringinvnz1ne0  20313  irredmul  20445  rnghmsscmap2  20645  rnghmsscmap  20646  rhmsscmap2  20674  rhmsscmap  20675  acsfn1p  20816  lspextmo  21072  lspsncv0  21165  pzriprnglem12  21520  psgnghm  21615  mplcoe1  22072  mplcoe5  22075  evlseu  22124  mhpsclcl  22168  mdetunilem7  22639  mdetunilem9  22641  chcoeffeq  22907  cnindis  23315  lmss  23321  lmcls  23325  lmcnp  23327  hausnei  23351  cmpsub  23423  tgcmp  23424  fiuncmp  23427  cmpfi  23431  bwth  23433  1stcrest  23476  2ndcdisj  23479  1stccnp  23485  comppfsc  23555  1stckgenlem  23576  txcls  23627  txcn  23649  txlm  23671  tx1stc  23673  xkococn  23683  hmphdis  23819  ptcmpfi  23836  isfild  23881  fgss2  23897  filconn  23906  trfil2  23910  ufileu  23942  filufint  23943  elfm2  23971  flftg  24019  fclssscls  24041  fclscf  24048  ufilcmp  24055  cnpfcf  24064  alexsubb  24069  alexsubALTlem4  24073  alexsubALT  24074  qustgpopn  24143  tsmsxp  24178  isust  24227  xmettri2  24365  blin2  24454  setsmstopn  24505  met2ndc  24551  metcnp3  24568  tngtopn  24686  reconnlem2  24862  xrge0tsms  24869  fsumcn  24907  bndth  25003  iscmet3lem2  25339  iscmet3  25340  ivthlem1  25499  ivthlem2  25500  ivthlem3  25501  ovolfiniun  25549  volfiniun  25595  ioombl1lem4  25609  ismbf3d  25702  mbfi1flimlem  25771  itg2seq  25791  itgfsum  25876  ellimc3  25928  dvmptfsum  26027  c1liplem1  26049  plypf1  26265  plydivex  26353  aannenlem1  26384  ulmval  26437  ulmcau  26452  ulmbdd  26455  ulmcn  26456  ulmdvlem3  26459  sineq0  26580  efopn  26714  cxpeq  26814  logbgcd1irr  26851  rlimcnp  27022  xrlimcnp  27025  lgsdir2lem2  27384  lgsne0  27393  2lgsoddprm  27474  2sqlem6  27481  2sqlem10  27486  2sqreunnltblem  27509  sltval2  27715  noetasuplem4  27795  conway  27858  madebdayim  27940  addsass  28052  zs12bday  28438  axcontlem2  28994  uhgr0vb  29103  uvtx01vtx  29428  uvtxupgrres  29439  fusgrn0degnn0  29531  finsumvtxdg2size  29582  cusgrm1rusgr  29614  wlkv0  29683  wlklenvclwlk  29687  uspgrn2crct  29837  frrusgrord  30369  numclwwlk1lem2fo  30386  isgrpo  30525  grpoidinvlem3  30534  vcdi  30593  vcdir  30594  vcass  30595  nvs  30691  nvtri  30698  blocnilem  30832  chintcli  31359  hsupss  31369  shlej1  31388  elspansn4  31601  spansncvi  31680  hoaddsub  31844  lnopl  31942  lnfnl  31959  riesz4i  32091  pjnormssi  32196  pj3si  32235  stlei  32268  stcltr2i  32303  dmdmd  32328  dmdbr5  32336  mdslmd1lem2  32354  atssma  32406  atcvatlem  32413  chirredlem1  32418  atcvat4i  32425  mdsymlem2  32432  mdsymlem6  32436  sumdmdlem2  32447  cdjreui  32460  elimifd  32563  disjxpin  32607  unifi3  32729  xrge0infss  32770  expgt0b  32822  xrge0tsmsd  33047  gsumle  33083  gsumvsca1  33214  gsumvsca2  33215  lmxrge0  33912  ismeas  34179  eulerpartlemb  34349  bnj849  34917  bnj1110  34974  srcmpltd  35072  swrdrevpfx  35100  cusgredgex2  35106  subgrwlk  35116  cusgr3cyclex  35120  umgr2cycllem  35124  umgr2cycl  35125  connpconn  35219  cvmseu  35260  cvmliftlem15  35282  cvmlift2lem1  35286  cvmlift2lem12  35298  satfv0fun  35355  satffunlem  35385  mclsind  35554  r1peuqusdeg1  35627  dfon2lem3  35766  dfon2lem4  35767  dfon2lem6  35769  dfon2lem8  35771  dfon2lem9  35772  hbntg  35786  cgrdegen  35985  funtransport  36012  ifscgr  36025  cgrxfr  36036  brofs2  36058  brifs2  36059  idinside  36065  btwnconn1lem7  36074  btwnconn1lem11  36078  btwnconn1lem12  36079  btwnconn1lem14  36081  broutsideof2  36103  btwnoutside  36106  outsideoftr  36110  in-ax8  36206  ss-ax8  36207  finminlem  36300  ntruni  36309  neibastop1  36341  ontgval  36413  ordtop  36418  ordcmp  36429  onint1  36431  bj-ax12w  36659  axc11n11r  36665  bj-ax12v3  36667  bj-nnfan  36730  bj-nnfand  36731  bj-nnflemea  36747  bj-19.42t  36755  bj-sbft  36757  bj-hbaeb2  36800  bj-spcimdv  36877  bj-spcimdvv  36878  bj-sngltag  36965  bj-xtagex  36971  bj-0int  37083  bj-ismooredr  37091  bj-inftyexpiinj  37191  nlpfvineqsn  37391  wl-ax13lem1  37476  wl-speqv  37502  wl-sbcom2d  37541  wl-ax11-lem3  37567  wl-ax11-lem8  37572  tan2h  37598  ptrest  37605  poimirlem20  37626  poimirlem22  37628  poimirlem26  37632  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  heicant  37641  voliunnfl  37650  volsupnfl  37651  itg2addnclem2  37658  itg2addnc  37660  itg2gt0cn  37661  ftc2nc  37688  filbcmb  37726  sdclem2  37728  seqpo  37733  nninfnub  37737  neificl  37739  prdstotbnd  37780  cnpwstotbnd  37783  heibor1lem  37795  heibor  37807  bfplem2  37809  opidonOLD  37838  exidu1  37842  grpokerinj  37879  rngoideu  37889  rngodi  37890  rngodir  37891  rngmgmbs4  37917  divrngidl  38014  prnc  38053  eqvrelqsel  38597  erimeq2  38659  prter2  38862  ax4fromc4  38875  hbae-o  38884  dvelimf-o  38910  ax12indn  38924  ax12inda2  38928  ax12a2-o  38931  l1cvpat  39035  atcvrj0  39410  pmaple  39743  paddasslem5  39806  pclfinN  39882  osumcllem11N  39948  pexmidlem8N  39959  dvheveccl  41094  dihord6apre  41238  lpolconN  41469  lcmineqlem1  42010  oexpreposd  42335  sn-it0e0  42421  cnreeu  42476  eu6w  42662  isnacs3  42697  pellexlem5  42820  pellex  42822  jm2.18  42976  jm2.15nn0  42991  jm2.16nn0  42992  dford3lem2  43015  ttac  43024  onexomgt  43229  onexoegt  43232  omabs2  43321  omcl3g  43323  tfsconcat0b  43335  naddgeoa  43383  safesnsupfiss  43404  rp-isfinite5  43506  cnvssb  43575  clcnvlem  43612  iunrelexpuztr  43708  rfovcnvf1od  43993  ntrrn  44111  nzss  44312  pm11.71  44392  axc11next  44401  hbntal  44550  eel2122old  44715  relwf  44941  modelaxreplem1  44942  ssclaxsep  44946  fsetsnf1  47001  2reu8i  47062  afvelima  47116  rlimdmafv  47126  rlimdmafv2  47207  elsprel  47399  sfprmdvdsmersenne  47527  perfectALTVlem2  47646  fpprwppr  47663  isuspgrim0lem  47808  uhgrimisgrgric  47836  gpgcubic  47969  gpg5nbgr3star  47971  copisnmnd  48012  funcringcsetcALTV2lem8  48140  funcringcsetclem8ALTV  48163  lindslinindsimp2lem5  48307  nn0sumshdig  48472  prelrrx2b  48563  itscnhlc0yqe  48608  iscnrm3lem2  48730  spd  48908  setrec1lem4  48920  setrec2fun  48922  aacllem  49031