Theorem syl5 35

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 32	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 33	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  37  syl2im  41  imim12i  63  pm2.86d  109  con2d  135  con3d  153  nsyli  158  biimtrid  245  biimtrrid  246  imbitrid  247  adantld  495  adantrd  496  impel  514  mpan9  515  pm4.72  964  pm2.36  985  pm4.79  1021  ecased  1051  alrimdh  1893  stdpc5v  1968  19.37imv  1977  ax12w  2168  ax13dgen2  2173  ax12v  2214  spsd  2223  nf5r  2230  axc4  2354  equs5eALT  2399  ax13lem1  2406  nfeqf  2413  hbae  2463  ax12vALT  2501  2ax6elem  2502  sb1  2510  euimmo  2644  necon2ad  2973  necon4ad  2977  r19.37v  3191  spcimgfi1OLD  3517  rr19.28v  3628  moeq3  3676  reuimrmo  3709  sbeqalb  3807  replem  5250  csbexg  5274  ralxfrd  5381  ralxfrd2  5385  ralxfrALT  5388  copsexgwOLD  5475  copsexg  5476  pwssun  5555  somo  5610  ssrel  5771  relssres  6023  dmsnopg  6216  dfco2a  6249  dfpo2  6299  frpoinsg  6346  tz7.7  6388  ordunidif  6413  suctr  6451  trsucss  6453  suc11  6472  imadif  6622  dffv2  6978  fvmptd3f  7007  fvmptnf  7014  foco2  7106  fconst5  7206  fvf1pr  7307  isores3  7335  riotaxfrd  7403  ovmpt4g  7559  ovmpos  7560  ov2gf  7561  ovmpodf  7568  sorpsscmpl  7733  abnexg  7756  onint  7790  limuni3  7849  tfisg  7851  tfis  7852  tfinds  7857  limomss  7868  peano5  7891  fo2ndf  8117  frxp  8123  xpord2pred  8142  xpord2indlem  8144  soseq  8156  suppss2  8197  suppssfv  8199  rntpos  8236  fprlem1  8298  fprresex  8308  wfr3g  8317  onfununi  8329  smofvon2  8344  smo11  8352  smoord  8353  tfrlem11  8376  tz7.44-2  8395  tz7.48lem  8429  tz7.48-1  8431  tz7.49  8433  tz7.49c  8434  omordi  8552  omord  8554  omass  8566  oneo  8567  omeulem1  8568  omopth2  8570  oewordri  8579  oeworde  8580  nnmordi  8618  nnmord  8619  omabs  8638  nnneo  8642  omsmo  8645  naddcllem  8663  qsel  8795  eceqoveq  8821  domunsncan  9066  sbthlem1  9076  2pwuninel  9121  mapen  9130  infensuc  9144  rexdif1en  9146  findcard2  9150  pssnn  9154  ssfi  9158  sucdom2  9188  php  9192  onomeneq  9199  0sdom1dom  9207  sdom1  9211  dif1ennnALT  9238  ac6sfi  9245  frfi  9246  unblem1  9253  unblem2  9254  unbnn2  9258  domunfican  9282  fodomfir  9288  ixpfi2  9308  finsschain  9317  unifi3  9320  marypha1lem  9394  oiexg  9498  brwdom3  9545  inf3lem2  9599  inf3lem3  9600  cantnfval2  9639  cantnflt  9642  cantnflem1  9659  cnfcom  9670  ttrclss  9690  trcl  9698  epfrs  9701  frmin  9722  frinsg  9724  frr3g  9729  frrlem15  9730  r1sdom  9747  cardsdomel  9961  carduni  9968  infpwfien  10047  carduniima  10081  dfac5  10113  dfac12r  10131  dfac12k  10132  kmlem11  10145  djuinf  10173  infxp  10198  cfsuc  10242  cfcoflem  10257  coftr  10258  infpssr  10293  fin23lem30  10327  isf32lem1  10338  isf34lem6  10365  fin1a2lem13  10397  fin1a2s  10399  axcc2lem  10421  domtriomlem  10427  axcclem  10442  ac6num  10464  zorn2lem5  10485  zorn2lem6  10486  axdclem2  10505  alephval2  10558  alephreg  10568  pwcfsdom  10569  axregndlem1  10588  axregnd  10590  axacndlem1  10593  axacndlem2  10594  axacndlem3  10595  axacndlem4  10596  axacnd  10598  gchi  10610  fpwwe2lem12  10628  canthp1  10640  gchpwdom  10656  wunfi  10707  tskwe2  10759  inar1  10761  gruen  10798  intgru  10800  indpi  10893  nqereu  10915  ltbtwnnq  10964  prnmadd  10983  genpcd  10992  prlem934  11019  ltexprlem1  11022  ltexprlem2  11023  ltexprlem7  11028  ltaprlem  11030  ltapr  11031  reclem4pr  11036  suplem2pr  11039  mulcmpblnr  11057  recexsrlem  11089  mulgt0sr  11091  supsrlem  11097  axpre-sup  11155  1re  11209  dedekindle  11375  addlsub  11631  recex  11847  nnunb  12501  0mnnnnn0  12537  prime  12678  zeo  12683  fnn0ind  12696  zindd  12698  btwnz  12700  lbzbi  12961  xrub  13339  elfznelfzo  13804  fvf1tp  13824  addmodlteq  13984  facwordi  14327  fiinfnf1o  14388  hashclb  14396  hashdom  14417  hashf1lem2  14495  seqcoll  14503  brfi1indALT  14549  ccatalpha  14633  pfxccatin12lem2a  14766  limsupbnd2  15536  rlimdm  15604  o1of2  15666  rlimno1  15707  isercoll  15721  caurcvg2  15731  caucvgb  15733  serf0  15734  zsum  15771  fsum2dlem  15823  fsum2d  15824  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  zprod  15993  fprod2dlem  16036  fprod2d  16037  odd2np1  16400  ndvdssub  16468  dfgcd2  16605  nprm  16747  maxprmfct  16769  rpexp  16782  pc2dvds  16940  pcfac  16960  unbenlem  16969  4sqlem12  17017  4sqlem17  17022  vdwlem13  17054  prmlem0  17166  mreiincl  17649  sscfn1  17875  initoid  18059  termoid  18060  funcestrcsetclem8  18204  funcsetcestrclem8  18219  pospo  18400  cnvpsb  18636  dirtr  18659  mulgaddcom  19165  mulginvcom  19166  gaass  19368  cntz2ss  19406  elsymgbas  19445  symgfix2  19487  pmtrfrn  19529  psgnran  19586  odmulg  19627  odhash3  19647  sylow2alem1  19688  sylow2alem2  19689  pj1eu  19767  efgs1b  19807  efgsfo  19810  efgredlemc  19816  efgredeu  19823  frgpuptinv  19842  lt6abl  19966  ghmcyg  19967  ablfac1eulem  20145  pgpfac1lem5  20152  ablsimpgfindlem1  20180  gsumle  20216  ringinvnz1ne0  20384  irredmul  20512  rnghmsscmap2  20715  rnghmsscmap  20716  rhmsscmap2  20744  rhmsscmap  20745  acsfn1p  20883  lspextmo  21158  lspsncv0  21251  pzriprnglem12  21623  psgnghm  21711  mplcoe1  22169  mplcoe5  22172  evlseu  22215  mhpsclcl  22291  mdetunilem7  22756  mdetunilem9  22758  chcoeffeq  23024  cnindis  23430  lmss  23436  lmcls  23440  lmcnp  23442  hausnei  23466  cmpsub  23538  tgcmp  23539  fiuncmp  23542  cmpfi  23546  bwth  23548  1stcrest  23591  2ndcdisj  23594  1stccnp  23600  comppfsc  23670  1stckgenlem  23691  txcls  23742  txcn  23764  txlm  23786  tx1stc  23788  xkococn  23798  hmphdis  23934  ptcmpfi  23951  isfild  23996  fgss2  24012  filconn  24021  trfil2  24025  ufileu  24057  filufint  24058  elfm2  24086  flftg  24134  fclssscls  24156  fclscf  24163  ufilcmp  24170  cnpfcf  24179  alexsubb  24184  alexsubALTlem4  24188  alexsubALT  24189  qustgpopn  24258  tsmsxp  24293  isust  24342  xmettri2  24478  blin2  24567  setsmstopn  24616  met2ndc  24661  metcnp3  24678  tngtopn  24788  reconnlem2  24966  xrge0tsms  24973  fsumcn  25010  bndth  25098  iscmet3lem2  25432  iscmet3  25433  ivthlem1  25591  ivthlem2  25592  ivthlem3  25593  ovolfiniun  25641  volfiniun  25687  ioombl1lem4  25701  ismbf3d  25794  mbfi1flimlem  25862  itg2seq  25882  itgfsum  25967  ellimc3  26019  dvmptfsum  26115  c1liplem1  26136  plypf1  26350  plydivex  26439  aannenlem1  26470  ulmval  26521  ulmcau  26536  ulmbdd  26539  ulmcn  26540  ulmdvlem3  26543  sineq0  26667  efopn  26801  cxpeq  26900  logbgcd1irr  26937  rlimcnp  27108  xrlimcnp  27111  lgsdir2lem2  27468  lgsne0  27477  2lgsoddprm  27558  2sqlem6  27565  2sqlem10  27570  2sqreunnltblem  27593  ltsval2  27798  noetasuplem4  27878  conway  27950  madebdayim  28059  addsass  28176  oncutlt  28435  oniso  28442  addonbday  28450  n0ssoldg  28524  bdayn0p1  28540  oldfib  28548  bdaypw2n0bndlem  28634  bdayfinbndlem1  28638  z12bdaylem1  28641  z12zsodd  28653  axcontlem2  29293  uhgr0vb  29400  uvtx01vtx  29725  uvtxupgrres  29736  fusgrn0degnn0  29827  finsumvtxdg2size  29878  cusgrm1rusgr  29910  wlkv0  29977  wlklenvclwlk  29981  uspgrn2crct  30135  frrusgrord  30670  numclwwlk1lem2fo  30687  isgrpo  30827  grpoidinvlem3  30836  vcdi  30895  vcdir  30896  vcass  30897  nvs  30993  nvtri  31000  blocnilem  31134  chintcli  31661  hsupss  31671  shlej1  31690  elspansn4  31903  spansncvi  31982  hoaddsub  32146  lnopl  32244  lnfnl  32261  riesz4i  32393  pjnormssi  32498  pj3si  32537  stlei  32570  stcltr2i  32605  dmdmd  32630  dmdbr5  32638  mdslmd1lem2  32656  atssma  32708  atcvatlem  32715  chirredlem1  32720  atcvat4i  32727  mdsymlem2  32734  mdsymlem6  32738  sumdmdlem2  32749  cdjreui  32762  elimifd  32867  disjxpin  32911  xrge0infss  33083  expgt0b  33139  xrge0tsmsd  33371  gsumvsca1  33524  gsumvsca2  33525  lmxrge0  34320  ismeas  34567  eulerpartlemb  34736  bnj849  35291  bnj1110  35348  srcmpltd  35447  axprALT2  35481  trssfir1om  35485  fineqvinfep  35516  trssfir1omregs  35527  swrdrevpfx  35586  cusgredgex2  35593  subgrwlk  35602  cusgr3cyclex  35606  umgr2cycllem  35610  umgr2cycl  35611  connpconn  35705  cvmseu  35746  cvmliftlem15  35768  cvmlift2lem1  35772  cvmlift2lem12  35784  satfv0fun  35841  satffunlem  35871  mclsind  36040  r1peuqusdeg1  36113  dfon2lem3  36253  dfon2lem4  36254  dfon2lem6  36256  dfon2lem8  36258  dfon2lem9  36259  hbntg  36273  cgrdegen  36474  funtransport  36501  ifscgr  36514  cgrxfr  36525  brofs2  36547  brifs2  36548  idinside  36554  btwnconn1lem7  36563  btwnconn1lem11  36567  btwnconn1lem12  36568  btwnconn1lem14  36570  broutsideof2  36592  btwnoutside  36595  outsideoftr  36599  nmulprop  36660  in-ax8  36714  ss-ax8  36715  finminlem  36807  ntruni  36816  neibastop1  36848  ontgval  36920  ordtop  36925  ordcmp  36936  onint1  36938  bj-alrimdh  37195  bj-spimnfe  37224  bj-spimenfa  37225  bj-cbveximd  37232  bj-spvew  37236  bj-cbvexvv  37240  bj-ax12w  37278  axc11n11r  37286  bj-ax12v3  37288  bj-nnfan  37357  bj-nnfand  37358  bj-19.42t  37368  bj-sbft  37381  bj-nnflemea  37392  bj-hbaeb2  37431  bj-spcimdv  37508  bj-spcimdvv  37509  bj-sngltag  37597  bj-xtagex  37603  bj-axseprep  37689  bj-0int  37721  bj-ismooredr  37729  bj-inftyexpiinj  37831  nlpfvineqsn  38033  wl-ax13lem1  38118  wl-speqv  38155  wl-sbcom2d  38194  tan2h  38241  ptrest  38248  poimirlem20  38269  poimirlem22  38271  poimirlem26  38275  poimirlem30  38279  poimirlem31  38280  poimirlem32  38281  heicant  38284  voliunnfl  38293  volsupnfl  38294  itg2addnclem2  38301  itg2addnc  38303  itg2gt0cn  38304  ftc2nc  38331  filbcmb  38369  sdclem2  38371  seqpo  38376  nninfnub  38380  neificl  38382  prdstotbnd  38423  cnpwstotbnd  38426  heibor1lem  38438  heibor  38450  bfplem2  38452  opidonOLD  38481  exidu1  38485  grpokerinj  38522  rngoideu  38532  rngodi  38533  rngodir  38534  rngmgmbs4  38560  divrngidl  38657  prnc  38696  rsp3eq  38994  eqvrelqsel  39327  erimeq2  39390  prter2  39633  ax4fromc4  39646  hbae-o  39655  dvelimf-o  39681  ax12indn  39695  ax12inda2  39699  ax12a2-o  39702  l1cvpat  39806  atcvrj0  40180  pmaple  40513  paddasslem5  40576  pclfinN  40652  osumcllem11N  40718  pexmidlem8N  40729  dvheveccl  41864  dihord6apre  42008  lpolconN  42239  lcmineqlem1  42774  oexpreposd  43061  sn-it0e0  43155  cnreeu  43242  eu6w  43388  isnacs3  43421  pellexlem5  43540  pellex  43542  jm2.18  43695  jm2.15nn0  43710  jm2.16nn0  43711  dford3lem2  43734  ttac  43743  onexomgt  43948  onexoegt  43951  omabs2  44039  omcl3g  44041  tfsconcat0b  44053  naddgeoa  44101  safesnsupfiss  44121  rp-isfinite5  44223  cnvssb  44292  clcnvlem  44329  iunrelexpuztr  44425  rfovcnvf1od  44710  ntrrn  44828  nzss  45007  pm11.71  45087  axc11next  45096  hbntal  45242  eel2122old  45406  relwf  45656  modelaxreplem1  45667  ssclaxsep  45671  wfac8prim  45691  fsetsnf1  47766  2reu8i  47827  afvelima  47881  rlimdmafv  47891  rlimdmafv2  47972  elsprel  48201  sfprmdvdsmersenne  48332  perfectALTVlem2  48464  fpprwppr  48481  uhgrimedgi  48632  isuspgrim0lem  48635  uhgrimisgrgric  48673  gpgcubic  48821  gpg5nbgr3star  48823  pgnioedg1  48850  pgnioedg2  48851  pgnioedg3  48852  pgnioedg4  48853  pgnioedg5  48854  copisnmnd  48911  funcringcsetcALTV2lem8  49039  funcringcsetclem8ALTV  49062  lindslinindsimp2lem5  49219  nn0sumshdig  49380  prelrrx2b  49471  itscnhlc0yqe  49516  iscnrm3lem2  49690  diag1f1lem  50061  spd  50433  setrec1lem4  50445  setrec2fun  50447  aacllem  50578