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  1863  stdpc5v  1938  19.37imv  1947  ax12w  2133  ax13dgen2  2138  ax12v  2178  spsd  2187  nf5r  2194  axc4  2321  equs5eALT  2369  ax13lem1  2378  nfeqf  2385  hbae  2435  ax12vALT  2473  2ax6elem  2474  sb1  2482  euimmo  2615  necon2ad  2947  necon4ad  2951  r19.37v  3167  spcimgfi1OLD  3527  rr19.28v  3647  moeq3  3695  reuimrmo  3728  sbeqalb  3828  csbexg  5280  ralxfrd  5378  ralxfrd2  5382  ralxfrALT  5385  copsexgw  5465  copsexg  5466  pwssun  5545  somo  5600  ssrel  5761  ssrelOLD  5762  relssres  6009  dmsnopg  6202  dfco2a  6235  dfpo2  6285  frpoinsg  6332  wfisgOLD  6343  tz7.7  6378  ordunidif  6402  suctr  6439  trsucss  6441  suc11  6460  imadif  6619  dffv2  6973  fvmptd3f  7000  fvmptnf  7007  foco2  7098  fconst5  7197  fvf1pr  7299  isores3  7327  riotaxfrd  7394  ovmpt4g  7552  ovmpos  7553  ov2gf  7554  ovmpodf  7561  sorpsscmpl  7726  abnexg  7748  onint  7782  limuni3  7845  tfisg  7847  tfis  7848  tfinds  7853  limomss  7864  peano5  7887  fo2ndf  8118  frxp  8123  xpord2pred  8142  xpord2indlem  8144  soseq  8156  suppss2  8197  suppssfv  8199  rntpos  8236  fprlem1  8297  fprresex  8307  wfr3g  8319  wfrlem5OLD  8325  wfrlem17OLD  8337  onfununi  8353  smofvon2  8368  smo11  8376  smoord  8377  tfrlem11  8400  tz7.44-2  8419  tz7.48lem  8453  tz7.48-1  8455  tz7.49  8457  tz7.49c  8458  omordi  8576  omord  8578  omass  8590  oneo  8591  omeulem1  8592  omopth2  8594  oewordri  8602  oeworde  8603  nnmordi  8641  nnmord  8642  omabs  8661  nnneo  8665  omsmo  8668  naddcllem  8686  qsel  8808  eceqoveq  8834  domunsncan  9084  sucdom2OLD  9094  sbthlem1  9095  2pwuninel  9144  mapen  9153  infensuc  9167  rexdif1en  9170  findcard2  9176  pssnn  9180  ssfi  9185  sucdom2  9215  php  9219  onomeneq  9235  0sdom1dom  9244  sdom1  9248  dif1ennnALT  9281  ac6sfi  9290  frfi  9291  unblem1  9298  unblem2  9299  unbnn2  9303  nnsdomgOLD  9306  xpfiOLD  9329  domunfican  9331  fiintOLD  9337  fodomfir  9338  ixpfi2  9360  finsschain  9369  marypha1lem  9443  oiexg  9547  brwdom3  9594  inf3lem2  9641  inf3lem3  9642  cantnfval2  9681  cantnflt  9684  cantnflem1  9701  cnfcom  9712  ttrclss  9732  trcl  9740  epfrs  9743  frmin  9761  frinsg  9763  frr3g  9768  frrlem15  9769  r1sdom  9786  cardsdomel  9986  carduni  9993  pr2neOLD  10017  infpwfien  10074  carduniima  10108  dfac5  10141  dfac12r  10159  dfac12k  10160  kmlem11  10173  djuinf  10201  infxp  10226  cfsuc  10269  cfcoflem  10284  coftr  10285  infpssr  10320  fin23lem30  10354  isf32lem1  10365  isf34lem6  10392  fin1a2lem13  10424  fin1a2s  10426  axcc2lem  10448  domtriomlem  10454  axcclem  10469  ac6num  10491  zorn2lem5  10512  zorn2lem6  10513  axdclem2  10532  alephval2  10584  alephreg  10594  pwcfsdom  10595  axregndlem1  10614  axregnd  10616  axacndlem1  10619  axacndlem2  10620  axacndlem3  10621  axacndlem4  10622  axacnd  10624  gchi  10636  fpwwe2lem12  10654  canthp1  10666  gchpwdom  10682  wunfi  10733  tskwe2  10785  inar1  10787  gruen  10824  intgru  10826  indpi  10919  nqereu  10941  ltbtwnnq  10990  prnmadd  11009  genpcd  11018  prlem934  11045  ltexprlem1  11048  ltexprlem2  11049  ltexprlem7  11054  ltaprlem  11056  ltapr  11057  reclem4pr  11062  suplem2pr  11065  mulcmpblnr  11083  recexsrlem  11115  mulgt0sr  11117  supsrlem  11123  axpre-sup  11181  1re  11233  dedekindle  11397  addlsub  11651  recex  11867  nnunb  12495  0mnnnnn0  12531  prime  12672  zeo  12677  fnn0ind  12690  zindd  12692  btwnz  12694  lbzbi  12950  xrub  13326  elfznelfzo  13786  fvf1tp  13804  addmodlteq  13962  facwordi  14305  fiinfnf1o  14366  hashclb  14374  hashdom  14395  hashf1lem2  14472  seqcoll  14480  brfi1indALT  14526  ccatalpha  14609  pfxccatin12lem2a  14743  limsupbnd2  15497  rlimdm  15565  o1of2  15627  rlimno1  15668  isercoll  15682  caurcvg2  15692  caucvgb  15694  serf0  15695  zsum  15732  fsum2dlem  15784  fsum2d  15785  fsumabs  15815  fsumrlim  15825  fsumo1  15826  fsumiun  15835  zprod  15951  fprod2dlem  15994  fprod2d  15995  odd2np1  16358  ndvdssub  16426  dfgcd2  16563  nprm  16705  maxprmfct  16726  rpexp  16739  pc2dvds  16897  pcfac  16917  unbenlem  16926  4sqlem12  16974  4sqlem17  16979  vdwlem13  17011  prmlem0  17123  mreiincl  17606  sscfn1  17828  initoid  18012  termoid  18013  funcestrcsetclem8  18157  funcsetcestrclem8  18172  pospo  18353  cnvpsb  18587  dirtr  18610  mulgaddcom  19079  mulginvcom  19080  gaass  19278  cntz2ss  19316  elsymgbas  19353  symgfix2  19395  pmtrfrn  19437  psgnran  19494  odmulg  19535  odhash3  19555  sylow2alem1  19596  sylow2alem2  19597  pj1eu  19675  efgs1b  19715  efgsfo  19718  efgredlemc  19724  efgredeu  19731  frgpuptinv  19750  lt6abl  19874  ghmcyg  19875  ablfac1eulem  20053  pgpfac1lem5  20060  ablsimpgfindlem1  20088  ringinvnz1ne0  20258  irredmul  20387  rnghmsscmap2  20587  rnghmsscmap  20588  rhmsscmap2  20616  rhmsscmap  20617  acsfn1p  20757  lspextmo  21012  lspsncv0  21105  pzriprnglem12  21451  psgnghm  21538  mplcoe1  21993  mplcoe5  21996  evlseu  22039  mhpsclcl  22083  mdetunilem7  22554  mdetunilem9  22556  chcoeffeq  22822  cnindis  23228  lmss  23234  lmcls  23238  lmcnp  23240  hausnei  23264  cmpsub  23336  tgcmp  23337  fiuncmp  23340  cmpfi  23344  bwth  23346  1stcrest  23389  2ndcdisj  23392  1stccnp  23398  comppfsc  23468  1stckgenlem  23489  txcls  23540  txcn  23562  txlm  23584  tx1stc  23586  xkococn  23596  hmphdis  23732  ptcmpfi  23749  isfild  23794  fgss2  23810  filconn  23819  trfil2  23823  ufileu  23855  filufint  23856  elfm2  23884  flftg  23932  fclssscls  23954  fclscf  23961  ufilcmp  23968  cnpfcf  23977  alexsubb  23982  alexsubALTlem4  23986  alexsubALT  23987  qustgpopn  24056  tsmsxp  24091  isust  24140  xmettri2  24277  blin2  24366  setsmstopn  24415  met2ndc  24460  metcnp3  24477  tngtopn  24587  reconnlem2  24765  xrge0tsms  24772  fsumcn  24810  bndth  24906  iscmet3lem2  25242  iscmet3  25243  ivthlem1  25402  ivthlem2  25403  ivthlem3  25404  ovolfiniun  25452  volfiniun  25498  ioombl1lem4  25512  ismbf3d  25605  mbfi1flimlem  25673  itg2seq  25693  itgfsum  25778  ellimc3  25830  dvmptfsum  25929  c1liplem1  25951  plypf1  26167  plydivex  26255  aannenlem1  26286  ulmval  26339  ulmcau  26354  ulmbdd  26357  ulmcn  26358  ulmdvlem3  26361  sineq0  26483  efopn  26617  cxpeq  26717  logbgcd1irr  26754  rlimcnp  26925  xrlimcnp  26928  lgsdir2lem2  27287  lgsne0  27296  2lgsoddprm  27377  2sqlem6  27384  2sqlem10  27389  2sqreunnltblem  27412  sltval2  27618  noetasuplem4  27698  conway  27761  madebdayim  27843  addsass  27955  zs12bday  28341  axcontlem2  28890  uhgr0vb  28997  uvtx01vtx  29322  uvtxupgrres  29333  fusgrn0degnn0  29425  finsumvtxdg2size  29476  cusgrm1rusgr  29508  wlkv0  29577  wlklenvclwlk  29581  uspgrn2crct  29736  frrusgrord  30268  numclwwlk1lem2fo  30285  isgrpo  30424  grpoidinvlem3  30433  vcdi  30492  vcdir  30493  vcass  30494  nvs  30590  nvtri  30597  blocnilem  30731  chintcli  31258  hsupss  31268  shlej1  31287  elspansn4  31500  spansncvi  31579  hoaddsub  31743  lnopl  31841  lnfnl  31858  riesz4i  31990  pjnormssi  32095  pj3si  32134  stlei  32167  stcltr2i  32202  dmdmd  32227  dmdbr5  32235  mdslmd1lem2  32253  atssma  32305  atcvatlem  32312  chirredlem1  32317  atcvat4i  32324  mdsymlem2  32331  mdsymlem6  32335  sumdmdlem2  32346  cdjreui  32359  elimifd  32470  disjxpin  32515  unifi3  32636  xrge0infss  32683  expgt0b  32741  xrge0tsmsd  33002  gsumle  33038  gsumvsca1  33169  gsumvsca2  33170  lmxrge0  33929  ismeas  34176  eulerpartlemb  34346  bnj849  34902  bnj1110  34959  srcmpltd  35057  swrdrevpfx  35085  cusgredgex2  35091  subgrwlk  35100  cusgr3cyclex  35104  umgr2cycllem  35108  umgr2cycl  35109  connpconn  35203  cvmseu  35244  cvmliftlem15  35266  cvmlift2lem1  35270  cvmlift2lem12  35282  satfv0fun  35339  satffunlem  35369  mclsind  35538  r1peuqusdeg1  35611  dfon2lem3  35749  dfon2lem4  35750  dfon2lem6  35752  dfon2lem8  35754  dfon2lem9  35755  hbntg  35769  cgrdegen  35968  funtransport  35995  ifscgr  36008  cgrxfr  36019  brofs2  36041  brifs2  36042  idinside  36048  btwnconn1lem7  36057  btwnconn1lem11  36061  btwnconn1lem12  36062  btwnconn1lem14  36064  broutsideof2  36086  btwnoutside  36089  outsideoftr  36093  in-ax8  36188  ss-ax8  36189  finminlem  36282  ntruni  36291  neibastop1  36323  ontgval  36395  ordtop  36400  ordcmp  36411  onint1  36413  bj-ax12w  36641  axc11n11r  36647  bj-ax12v3  36649  bj-nnfan  36712  bj-nnfand  36713  bj-nnflemea  36729  bj-19.42t  36737  bj-sbft  36739  bj-hbaeb2  36782  bj-spcimdv  36859  bj-spcimdvv  36860  bj-sngltag  36947  bj-xtagex  36953  bj-0int  37065  bj-ismooredr  37073  bj-inftyexpiinj  37173  nlpfvineqsn  37373  wl-ax13lem1  37458  wl-speqv  37486  wl-sbcom2d  37525  wl-ax11-lem3  37551  wl-ax11-lem8  37556  tan2h  37582  ptrest  37589  poimirlem20  37610  poimirlem22  37612  poimirlem26  37616  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  heicant  37625  voliunnfl  37634  volsupnfl  37635  itg2addnclem2  37642  itg2addnc  37644  itg2gt0cn  37645  ftc2nc  37672  filbcmb  37710  sdclem2  37712  seqpo  37717  nninfnub  37721  neificl  37723  prdstotbnd  37764  cnpwstotbnd  37767  heibor1lem  37779  heibor  37791  bfplem2  37793  opidonOLD  37822  exidu1  37826  grpokerinj  37863  rngoideu  37873  rngodi  37874  rngodir  37875  rngmgmbs4  37901  divrngidl  37998  prnc  38037  eqvrelqsel  38580  erimeq2  38642  prter2  38845  ax4fromc4  38858  hbae-o  38867  dvelimf-o  38893  ax12indn  38907  ax12inda2  38911  ax12a2-o  38914  l1cvpat  39018  atcvrj0  39393  pmaple  39726  paddasslem5  39789  pclfinN  39865  osumcllem11N  39931  pexmidlem8N  39942  dvheveccl  41077  dihord6apre  41221  lpolconN  41452  lcmineqlem1  41988  oexpreposd  42318  sn-it0e0  42405  cnreeu  42460  eu6w  42646  isnacs3  42680  pellexlem5  42803  pellex  42805  jm2.18  42959  jm2.15nn0  42974  jm2.16nn0  42975  dford3lem2  42998  ttac  43007  onexomgt  43212  onexoegt  43215  omabs2  43303  omcl3g  43305  tfsconcat0b  43317  naddgeoa  43365  safesnsupfiss  43386  rp-isfinite5  43488  cnvssb  43557  clcnvlem  43594  iunrelexpuztr  43690  rfovcnvf1od  43975  ntrrn  44093  nzss  44289  pm11.71  44369  axc11next  44378  hbntal  44526  eel2122old  44690  relwf  44940  modelaxreplem1  44951  ssclaxsep  44955  wfac8prim  44975  fsetsnf1  47029  2reu8i  47090  afvelima  47144  rlimdmafv  47154  rlimdmafv2  47235  elsprel  47437  sfprmdvdsmersenne  47565  perfectALTVlem2  47684  fpprwppr  47701  uhgrimedgi  47851  isuspgrim0lem  47854  uhgrimisgrgric  47892  gpgcubic  48029  gpg5nbgr3star  48031  copisnmnd  48092  funcringcsetcALTV2lem8  48220  funcringcsetclem8ALTV  48243  lindslinindsimp2lem5  48386  nn0sumshdig  48551  prelrrx2b  48642  itscnhlc0yqe  48687  iscnrm3lem2  48857  diag1f1lem  49165  spd  49490  setrec1lem4  49502  setrec2fun  49504  aacllem  49613