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  1019  ecased  1049  alrimdh  1886  stdpc5v  1961  19.37imv  1970  ax12w  2170  ax13dgen2  2175  ax12v  2216  spsd  2225  nf5r  2232  axc4  2356  equs5eALT  2401  ax13lem1  2408  nfeqf  2415  hbae  2465  ax12vALT  2503  2ax6elem  2504  sb1  2512  euimmo  2646  necon2ad  2975  necon4ad  2979  r19.37v  3191  spcimgfi1OLD  3519  rr19.28v  3630  moeq3  3678  reuimrmo  3711  sbeqalb  3809  replem  5243  csbexg  5265  ralxfrd  5370  ralxfrd2  5374  ralxfrALT  5377  copsexgwOLD  5464  copsexg  5465  pwssun  5544  somo  5599  ssrel  5760  relssres  6012  dmsnopg  6204  dfco2a  6237  dfpo2  6287  frpoinsg  6334  tz7.7  6376  ordunidif  6400  suctr  6438  trsucss  6440  suc11  6459  imadif  6609  dffv2  6966  fvmptd3f  6995  fvmptnf  7002  foco2  7094  fconst5  7194  fvf1pr  7295  isores3  7323  riotaxfrd  7391  ovmpt4g  7547  ovmpos  7548  ov2gf  7549  ovmpodf  7556  sorpsscmpl  7721  abnexg  7743  onint  7777  limuni3  7836  tfisg  7838  tfis  7839  tfinds  7844  limomss  7855  peano5  7878  fo2ndf  8104  frxp  8110  xpord2pred  8129  xpord2indlem  8131  soseq  8143  suppss2  8184  suppssfv  8186  rntpos  8223  fprlem1  8285  fprresex  8295  wfr3g  8304  onfununi  8316  smofvon2  8331  smo11  8339  smoord  8340  tfrlem11  8363  tz7.44-2  8382  tz7.48lem  8416  tz7.48-1  8418  tz7.49  8420  tz7.49c  8421  omordi  8539  omord  8541  omass  8553  oneo  8554  omeulem1  8555  omopth2  8557  oewordri  8566  oeworde  8567  nnmordi  8605  nnmord  8606  omabs  8625  nnneo  8629  omsmo  8632  naddcllem  8650  qsel  8782  eceqoveq  8808  domunsncan  9053  sbthlem1  9063  2pwuninel  9108  mapen  9117  infensuc  9131  rexdif1en  9133  findcard2  9137  pssnn  9141  ssfi  9145  sucdom2  9175  php  9179  onomeneq  9186  0sdom1dom  9194  sdom1  9198  dif1ennnALT  9225  ac6sfi  9232  frfi  9233  unblem1  9240  unblem2  9241  unbnn2  9245  domunfican  9269  fodomfir  9275  ixpfi2  9295  finsschain  9304  unifi3  9307  marypha1lem  9381  oiexg  9485  brwdom3  9532  inf3lem2  9586  inf3lem3  9587  cantnfval2  9626  cantnflt  9629  cantnflem1  9646  cnfcom  9657  ttrclss  9677  trcl  9685  epfrs  9688  frmin  9709  frinsg  9711  frr3g  9716  frrlem15  9717  r1sdom  9734  cardsdomel  9948  carduni  9955  infpwfien  10034  carduniima  10068  dfac5  10100  dfac12r  10118  dfac12k  10119  kmlem11  10132  djuinf  10160  infxp  10185  cfsuc  10229  cfcoflem  10244  coftr  10245  infpssr  10280  fin23lem30  10314  isf32lem1  10325  isf34lem6  10352  fin1a2lem13  10384  fin1a2s  10386  axcc2lem  10408  domtriomlem  10414  axcclem  10429  ac6num  10451  zorn2lem5  10472  zorn2lem6  10473  axdclem2  10492  alephval2  10545  alephreg  10555  pwcfsdom  10556  axregndlem1  10575  axregnd  10577  axacndlem1  10580  axacndlem2  10581  axacndlem3  10582  axacndlem4  10583  axacnd  10585  gchi  10597  fpwwe2lem12  10615  canthp1  10627  gchpwdom  10643  wunfi  10694  tskwe2  10746  inar1  10748  gruen  10785  intgru  10787  indpi  10880  nqereu  10902  ltbtwnnq  10951  prnmadd  10970  genpcd  10979  prlem934  11006  ltexprlem1  11009  ltexprlem2  11010  ltexprlem7  11015  ltaprlem  11017  ltapr  11018  reclem4pr  11023  suplem2pr  11026  mulcmpblnr  11044  recexsrlem  11076  mulgt0sr  11078  supsrlem  11084  axpre-sup  11142  1re  11196  dedekindle  11362  addlsub  11618  recex  11834  nnunb  12491  0mnnnnn0  12527  prime  12668  zeo  12673  fnn0ind  12686  zindd  12688  btwnz  12690  lbzbi  12951  xrub  13329  elfznelfzo  13793  fvf1tp  13813  addmodlteq  13973  facwordi  14316  fiinfnf1o  14377  hashclb  14385  hashdom  14406  hashf1lem2  14483  seqcoll  14491  brfi1indALT  14537  ccatalpha  14621  pfxccatin12lem2a  14754  limsupbnd2  15524  rlimdm  15592  o1of2  15654  rlimno1  15695  isercoll  15709  caurcvg2  15719  caucvgb  15721  serf0  15722  zsum  15759  fsum2dlem  15811  fsum2d  15812  fsumabs  15843  fsumrlim  15853  fsumo1  15854  fsumiun  15863  zprod  15981  fprod2dlem  16024  fprod2d  16025  odd2np1  16389  ndvdssub  16457  dfgcd2  16594  nprm  16736  maxprmfct  16758  rpexp  16771  pc2dvds  16929  pcfac  16949  unbenlem  16958  4sqlem12  17006  4sqlem17  17011  vdwlem13  17043  prmlem0  17155  mreiincl  17638  sscfn1  17864  initoid  18048  termoid  18049  funcestrcsetclem8  18193  funcsetcestrclem8  18208  pospo  18389  cnvpsb  18625  dirtr  18648  mulgaddcom  19155  mulginvcom  19156  gaass  19358  cntz2ss  19396  elsymgbas  19435  symgfix2  19477  pmtrfrn  19519  psgnran  19576  odmulg  19617  odhash3  19637  sylow2alem1  19678  sylow2alem2  19679  pj1eu  19757  efgs1b  19797  efgsfo  19800  efgredlemc  19806  efgredeu  19813  frgpuptinv  19832  lt6abl  19956  ghmcyg  19957  ablfac1eulem  20135  pgpfac1lem5  20142  ablsimpgfindlem1  20170  gsumle  20206  ringinvnz1ne0  20374  irredmul  20502  rnghmsscmap2  20705  rnghmsscmap  20706  rhmsscmap2  20734  rhmsscmap  20735  acsfn1p  20871  lspextmo  21146  lspsncv0  21239  pzriprnglem12  21602  psgnghm  21690  mplcoe1  22148  mplcoe5  22151  evlseu  22194  mhpsclcl  22270  mdetunilem7  22736  mdetunilem9  22738  chcoeffeq  23004  cnindis  23410  lmss  23416  lmcls  23420  lmcnp  23422  hausnei  23446  cmpsub  23518  tgcmp  23519  fiuncmp  23522  cmpfi  23526  bwth  23528  1stcrest  23571  2ndcdisj  23574  1stccnp  23580  comppfsc  23650  1stckgenlem  23671  txcls  23722  txcn  23744  txlm  23766  tx1stc  23768  xkococn  23778  hmphdis  23914  ptcmpfi  23931  isfild  23976  fgss2  23992  filconn  24001  trfil2  24005  ufileu  24037  filufint  24038  elfm2  24066  flftg  24114  fclssscls  24136  fclscf  24143  ufilcmp  24150  cnpfcf  24159  alexsubb  24164  alexsubALTlem4  24168  alexsubALT  24169  qustgpopn  24238  tsmsxp  24273  isust  24322  xmettri2  24458  blin2  24547  setsmstopn  24596  met2ndc  24641  metcnp3  24658  tngtopn  24768  reconnlem2  24946  xrge0tsms  24953  fsumcn  24990  bndth  25078  iscmet3lem2  25412  iscmet3  25413  ivthlem1  25571  ivthlem2  25572  ivthlem3  25573  ovolfiniun  25621  volfiniun  25667  ioombl1lem4  25681  ismbf3d  25774  mbfi1flimlem  25842  itg2seq  25862  itgfsum  25947  ellimc3  25999  dvmptfsum  26095  c1liplem1  26116  plypf1  26330  plydivex  26419  aannenlem1  26450  ulmval  26501  ulmcau  26516  ulmbdd  26519  ulmcn  26520  ulmdvlem3  26523  sineq0  26647  efopn  26781  cxpeq  26880  logbgcd1irr  26917  rlimcnp  27088  xrlimcnp  27091  lgsdir2lem2  27448  lgsne0  27457  2lgsoddprm  27538  2sqlem6  27545  2sqlem10  27550  2sqreunnltblem  27573  ltsval2  27778  noetasuplem4  27858  conway  27930  madebdayim  28039  addsass  28156  oncutlt  28415  oniso  28422  addonbday  28430  n0ssoldg  28504  bdayn0p1  28520  oldfib  28528  bdaypw2n0bndlem  28614  bdayfinbndlem1  28618  z12bdaylem1  28621  z12zsodd  28633  axcontlem2  29224  uhgr0vb  29331  uvtx01vtx  29656  uvtxupgrres  29667  fusgrn0degnn0  29758  finsumvtxdg2size  29809  cusgrm1rusgr  29841  wlkv0  29908  wlklenvclwlk  29912  uspgrn2crct  30066  frrusgrord  30601  numclwwlk1lem2fo  30618  isgrpo  30758  grpoidinvlem3  30767  vcdi  30826  vcdir  30827  vcass  30828  nvs  30924  nvtri  30931  blocnilem  31065  chintcli  31592  hsupss  31602  shlej1  31621  elspansn4  31834  spansncvi  31913  hoaddsub  32077  lnopl  32175  lnfnl  32192  riesz4i  32324  pjnormssi  32429  pj3si  32468  stlei  32501  stcltr2i  32536  dmdmd  32561  dmdbr5  32569  mdslmd1lem2  32587  atssma  32639  atcvatlem  32646  chirredlem1  32651  atcvat4i  32658  mdsymlem2  32665  mdsymlem6  32669  sumdmdlem2  32680  cdjreui  32693  elimifd  32799  disjxpin  32843  xrge0infss  33017  expgt0b  33074  xrge0tsmsd  33306  gsumvsca1  33459  gsumvsca2  33460  lmxrge0  34259  ismeas  34506  eulerpartlemb  34675  bnj849  35230  bnj1110  35287  srcmpltd  35385  axprALT2  35417  trssfir1om  35419  fineqvinfep  35433  trssfir1omregs  35444  swrdrevpfx  35479  cusgredgex2  35486  subgrwlk  35495  cusgr3cyclex  35499  umgr2cycllem  35503  umgr2cycl  35504  connpconn  35598  cvmseu  35639  cvmliftlem15  35661  cvmlift2lem1  35665  cvmlift2lem12  35677  satfv0fun  35734  satffunlem  35764  mclsind  35933  r1peuqusdeg1  36006  dfon2lem3  36146  dfon2lem4  36147  dfon2lem6  36149  dfon2lem8  36151  dfon2lem9  36152  hbntg  36166  cgrdegen  36367  funtransport  36394  ifscgr  36407  cgrxfr  36418  brofs2  36440  brifs2  36441  idinside  36447  btwnconn1lem7  36456  btwnconn1lem11  36460  btwnconn1lem12  36461  btwnconn1lem14  36463  broutsideof2  36485  btwnoutside  36488  outsideoftr  36492  nmulprop  36553  in-ax8  36597  ss-ax8  36598  finminlem  36691  ntruni  36700  neibastop1  36732  ontgval  36804  ordtop  36809  ordcmp  36820  onint1  36822  bj-alrimdh  37079  bj-spimnfe  37108  bj-spimenfa  37109  bj-cbveximd  37116  bj-spvew  37120  bj-cbvexvv  37124  bj-ax12w  37162  axc11n11r  37170  bj-ax12v3  37172  bj-nnfan  37241  bj-nnfand  37242  bj-19.42t  37252  bj-sbft  37265  bj-nnflemea  37276  bj-hbaeb2  37315  bj-spcimdv  37392  bj-spcimdvv  37393  bj-sngltag  37480  bj-xtagex  37486  bj-axseprep  37571  bj-0int  37603  bj-ismooredr  37611  bj-inftyexpiinj  37713  nlpfvineqsn  37915  wl-ax13lem1  38000  wl-speqv  38037  wl-sbcom2d  38076  tan2h  38123  ptrest  38130  poimirlem20  38151  poimirlem22  38153  poimirlem26  38157  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  heicant  38166  voliunnfl  38175  volsupnfl  38176  itg2addnclem2  38183  itg2addnc  38185  itg2gt0cn  38186  ftc2nc  38213  filbcmb  38251  sdclem2  38253  seqpo  38258  nninfnub  38262  neificl  38264  prdstotbnd  38305  cnpwstotbnd  38308  heibor1lem  38320  heibor  38332  bfplem2  38334  opidonOLD  38363  exidu1  38367  grpokerinj  38404  rngoideu  38414  rngodi  38415  rngodir  38416  rngmgmbs4  38442  divrngidl  38539  prnc  38578  rsp3eq  38878  eqvrelqsel  39211  erimeq2  39274  prter2  39517  ax4fromc4  39530  hbae-o  39539  dvelimf-o  39565  ax12indn  39579  ax12inda2  39583  ax12a2-o  39586  l1cvpat  39690  atcvrj0  40064  pmaple  40397  paddasslem5  40460  pclfinN  40536  osumcllem11N  40602  pexmidlem8N  40613  dvheveccl  41748  dihord6apre  41892  lpolconN  42123  lcmineqlem1  42658  oexpreposd  42943  sn-it0e0  43037  cnreeu  43124  eu6w  43270  isnacs3  43303  pellexlem5  43422  pellex  43424  jm2.18  43577  jm2.15nn0  43592  jm2.16nn0  43593  dford3lem2  43616  ttac  43625  onexomgt  43830  onexoegt  43833  omabs2  43921  omcl3g  43923  tfsconcat0b  43935  naddgeoa  43983  safesnsupfiss  44003  rp-isfinite5  44105  cnvssb  44174  clcnvlem  44211  iunrelexpuztr  44307  rfovcnvf1od  44592  ntrrn  44710  nzss  44891  pm11.71  44971  axc11next  44980  hbntal  45127  eel2122old  45291  relwf  45541  modelaxreplem1  45552  ssclaxsep  45556  wfac8prim  45576  fsetsnf1  47644  2reu8i  47705  afvelima  47759  rlimdmafv  47769  rlimdmafv2  47850  elsprel  48079  sfprmdvdsmersenne  48210  perfectALTVlem2  48342  fpprwppr  48359  uhgrimedgi  48510  isuspgrim0lem  48513  uhgrimisgrgric  48551  gpgcubic  48699  gpg5nbgr3star  48701  pgnioedg1  48728  pgnioedg2  48729  pgnioedg3  48730  pgnioedg4  48731  pgnioedg5  48732  copisnmnd  48789  funcringcsetcALTV2lem8  48917  funcringcsetclem8ALTV  48940  lindslinindsimp2lem5  49093  nn0sumshdig  49254  prelrrx2b  49345  itscnhlc0yqe  49390  iscnrm3lem2  49564  diag1f1lem  49935  spd  50307  setrec1lem4  50319  setrec2fun  50321  aacllem  50430