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  syl5bi  241  syl5bir  242  syl5ib  243  adantld  490  adantrd  491  impel  505  mpan9  506  pm4.72  946  pm2.36  966  pm4.79  1000  ecased  1031  ecase3adOLD  1033  alrimdh  1869  stdpc5v  1944  19.37imv  1954  ax12w  2132  ax13dgen2  2137  ax12v  2175  spsd  2183  nf5r  2190  axc4  2318  equs5eALT  2366  ax13lem1  2375  nfeqf  2382  hbae  2432  ax12vALT  2470  2ax6elem  2471  sb1  2480  euimmo  2619  necon2ad  2959  necon4ad  2963  r19.37v  3273  spcimgft  3524  rr19.28v  3600  moeq3  3650  reuimrmo  3683  sbeqalb  3788  csbexg  5237  ralxfrd  5334  ralxfrd2  5338  ralxfrALT  5341  copsexgw  5406  copsexg  5407  pwssun  5484  somo  5539  ssrel  5691  relssres  5929  dmsnopg  6113  dfco2a  6147  dfpo2  6196  frpoinsg  6243  wfisgOLD  6254  tz7.7  6289  ordunidif  6311  suctr  6346  trsucss  6348  suc11  6366  imadif  6514  dffv2  6857  fvmptd3f  6884  fvmptnf  6891  foco2  6977  fconst5  7075  isores3  7199  riotaxfrd  7260  ovmpt4g  7411  ovmpos  7412  ov2gf  7413  ovmpodf  7420  sorpsscmpl  7578  abnexg  7597  onint  7630  limuni3  7687  tfis  7689  tfinds  7694  limomss  7705  peano5  7727  peano5OLD  7728  fo2ndf  7946  frxp  7951  suppss2  8000  suppssfv  8002  rntpos  8039  fprlem1  8100  fprresex  8110  wfr3g  8122  wfrlem5OLD  8128  wfrlem17OLD  8140  onfununi  8156  smofvon2  8171  smo11  8179  smoord  8180  tfrlem11  8203  tz7.44-2  8222  tz7.48lem  8256  tz7.48-1  8258  tz7.49  8260  tz7.49c  8261  omordi  8373  omord  8375  omass  8387  oneo  8388  omeulem1  8389  omopth2  8391  oewordri  8399  oeworde  8400  nnmordi  8438  nnmord  8439  omabs  8455  nnneo  8459  omsmo  8462  qsel  8559  eceqoveq  8585  domunsncan  8828  sucdom2  8838  sbthlem1  8839  2pwuninel  8884  mapen  8893  infensuc  8907  findcard2  8912  pssnn  8916  ssfi  8921  php  8957  pssnnOLD  9001  dif1enALT  9011  findcard2OLD  9017  ac6sfi  9019  frfi  9020  unblem1  9027  unblem2  9028  unbnn2  9032  nnsdomg  9034  xpfi  9046  domunfican  9048  fiint  9052  ixpfi2  9078  finsschain  9087  marypha1lem  9153  oiexg  9255  brwdom3  9302  inf3lem2  9348  inf3lem3  9349  cantnfval2  9388  cantnflt  9391  cantnflem1  9408  cnfcom  9419  ttrclss  9439  dftrpred3g  9464  trpredrec  9467  trcl  9469  epfrs  9472  frmin  9490  frinsg  9493  frr3g  9498  frrlem15  9499  r1sdom  9516  cardsdomel  9716  carduni  9723  pr2ne  9745  infpwfien  9802  carduniima  9836  dfac5  9868  dfac12r  9886  dfac12k  9887  kmlem11  9900  djuinf  9928  infxp  9955  cfsuc  9997  cfcoflem  10012  coftr  10013  infpssr  10048  fin23lem30  10082  isf32lem1  10093  isf34lem6  10120  fin1a2lem13  10152  fin1a2s  10154  axcc2lem  10176  domtriomlem  10182  axcclem  10197  ac6num  10219  zorn2lem5  10240  zorn2lem6  10241  axdclem2  10260  alephval2  10312  alephreg  10322  pwcfsdom  10323  axregndlem1  10342  axregnd  10344  axacndlem1  10347  axacndlem2  10348  axacndlem3  10349  axacndlem4  10350  axacnd  10352  gchi  10364  fpwwe2lem12  10382  canthp1  10394  gchpwdom  10410  wunfi  10461  tskwe2  10513  inar1  10515  gruen  10552  intgru  10554  indpi  10647  nqereu  10669  ltbtwnnq  10718  prnmadd  10737  genpcd  10746  prlem934  10773  ltexprlem1  10776  ltexprlem2  10777  ltexprlem7  10782  ltaprlem  10784  ltapr  10785  reclem4pr  10790  suplem2pr  10793  mulcmpblnr  10811  recexsrlem  10843  mulgt0sr  10845  supsrlem  10851  axpre-sup  10909  1re  10959  dedekindle  11122  addlsub  11374  recex  11590  nnunb  12212  0mnnnnn0  12248  prime  12384  zeo  12389  fnn0ind  12402  zindd  12404  btwnz  12405  lbzbi  12658  xrub  13028  elfznelfzo  13473  addmodlteq  13647  facwordi  13984  fiinfnf1o  14045  hashclb  14054  hashdom  14075  hashf1lem2  14151  seqcoll  14159  brfi1indALT  14195  ccatalpha  14279  pfxccatin12lem2a  14421  limsupbnd2  15173  rlimdm  15241  o1of2  15303  rlimno1  15346  isercoll  15360  caurcvg2  15370  caucvgb  15372  serf0  15373  zsum  15411  fsum2dlem  15463  fsum2d  15464  fsumabs  15494  fsumrlim  15504  fsumo1  15505  fsumiun  15514  zprod  15628  fprod2dlem  15671  fprod2d  15672  odd2np1  16031  ndvdssub  16099  dfgcd2  16235  nprm  16374  maxprmfct  16395  rpexp  16408  pc2dvds  16561  pcfac  16581  unbenlem  16590  4sqlem12  16638  4sqlem17  16643  vdwlem13  16675  prmlem0  16788  mreiincl  17286  sscfn1  17510  initoid  17697  termoid  17698  funcestrcsetclem8  17845  funcsetcestrclem8  17860  pospo  18044  cnvpsb  18278  dirtr  18301  mulgaddcom  18708  mulginvcom  18709  gaass  18884  cntz2ss  18920  elsymgbas  18962  symgfix2  19005  pmtrfrn  19047  psgnran  19104  odmulg  19144  odhash3  19162  sylow2alem1  19203  sylow2alem2  19204  pj1eu  19283  efgs1b  19323  efgsfo  19326  efgredlemc  19332  efgredeu  19339  frgpuptinv  19358  lt6abl  19477  ghmcyg  19478  ablfac1eulem  19656  pgpfac1lem5  19663  ablsimpgfindlem1  19691  ringinvnz1ne0  19812  irredmul  19932  acsfn1p  20048  lspextmo  20299  lspsncv0  20389  psgnghm  20766  mplcoe1  21219  mplcoe5  21222  evlseu  21274  mhpsclcl  21318  mdetunilem7  21748  mdetunilem9  21750  chcoeffeq  22016  cnindis  22424  lmss  22430  lmcls  22434  lmcnp  22436  hausnei  22460  cmpsub  22532  tgcmp  22533  fiuncmp  22536  cmpfi  22540  bwth  22542  1stcrest  22585  2ndcdisj  22588  1stccnp  22594  comppfsc  22664  1stckgenlem  22685  txcls  22736  txcn  22758  txlm  22780  tx1stc  22782  xkococn  22792  hmphdis  22928  ptcmpfi  22945  isfild  22990  fgss2  23006  filconn  23015  trfil2  23019  ufileu  23051  filufint  23052  elfm2  23080  flftg  23128  fclssscls  23150  fclscf  23157  ufilcmp  23164  cnpfcf  23173  alexsubb  23178  alexsubALTlem4  23182  alexsubALT  23183  qustgpopn  23252  tsmsxp  23287  isust  23336  xmettri2  23474  blin2  23563  setsmstopn  23614  met2ndc  23660  metcnp3  23677  tngtopn  23795  reconnlem2  23971  xrge0tsms  23978  fsumcn  24014  bndth  24102  iscmet3lem2  24437  iscmet3  24438  ivthlem1  24596  ivthlem2  24597  ivthlem3  24598  ovolfiniun  24646  volfiniun  24692  ioombl1lem4  24706  ismbf3d  24799  mbfi1flimlem  24868  itg2seq  24888  itgfsum  24972  ellimc3  25024  dvmptfsum  25120  c1liplem1  25141  plypf1  25354  plydivex  25438  aannenlem1  25469  ulmval  25520  ulmcau  25535  ulmbdd  25538  ulmcn  25539  ulmdvlem3  25542  sineq0  25661  efopn  25794  cxpeq  25891  logbgcd1irr  25925  rlimcnp  26096  xrlimcnp  26099  lgsdir2lem2  26455  lgsne0  26464  2lgsoddprm  26545  2sqlem6  26552  2sqlem10  26557  2sqreunnltblem  26580  axcontlem2  27314  uhgr0vb  27423  uvtx01vtx  27745  uvtxupgrres  27756  fusgrn0degnn0  27847  finsumvtxdg2size  27898  cusgrm1rusgr  27930  wlkv0  27998  wlklenvclwlk  28002  uspgrn2crct  28152  frrusgrord  28684  numclwwlk1lem2fo  28701  isgrpo  28838  grpoidinvlem3  28847  vcdi  28906  vcdir  28907  vcass  28908  nvs  29004  nvtri  29011  blocnilem  29145  chintcli  29672  hsupss  29682  shlej1  29701  elspansn4  29914  spansncvi  29993  hoaddsub  30157  lnopl  30255  lnfnl  30272  riesz4i  30404  pjnormssi  30509  pj3si  30548  stlei  30581  stcltr2i  30616  dmdmd  30641  dmdbr5  30649  mdslmd1lem2  30667  atssma  30719  atcvatlem  30726  chirredlem1  30731  atcvat4i  30738  mdsymlem2  30745  mdsymlem6  30749  sumdmdlem2  30760  cdjreui  30773  elimifd  30865  disjxpin  30906  unifi3  31026  xrge0infss  31062  xrge0tsmsd  31296  gsumle  31329  gsumvsca1  31458  gsumvsca2  31459  lmxrge0  31881  ismeas  32146  eulerpartlemb  32314  bnj849  32884  bnj1110  32941  srcmpltd  33033  swrdrevpfx  33057  cusgredgex2  33063  subgrwlk  33073  cusgr3cyclex  33077  umgr2cycllem  33081  umgr2cycl  33082  connpconn  33176  cvmseu  33217  cvmliftlem15  33239  cvmlift2lem1  33243  cvmlift2lem12  33255  satfv0fun  33312  satffunlem  33342  mclsind  33511  dfon2lem3  33740  dfon2lem4  33741  dfon2lem6  33743  dfon2lem8  33745  dfon2lem9  33746  hbntg  33760  tfisg  33765  xpord2pred  33771  xpord2ind  33773  xpord3ind  33779  soseq  33782  naddcllem  33810  sltval2  33838  noetasuplem4  33918  conway  33972  madebdayim  34049  cgrdegen  34285  funtransport  34312  ifscgr  34325  cgrxfr  34336  brofs2  34358  brifs2  34359  idinside  34365  btwnconn1lem7  34374  btwnconn1lem11  34378  btwnconn1lem12  34379  btwnconn1lem14  34381  broutsideof2  34403  btwnoutside  34406  outsideoftr  34410  finminlem  34486  ntruni  34495  neibastop1  34527  ontgval  34599  ordtop  34604  ordcmp  34615  onint1  34617  bj-ax12w  34837  axc11n11r  34844  bj-ax12v3  34846  bj-nnfan  34909  bj-nnfand  34910  bj-nnflemea  34926  bj-19.42t  34934  bj-sbft  34936  bj-hbaeb2  34980  bj-spcimdv  35059  bj-spcimdvv  35060  bj-sngltag  35152  bj-xtagex  35158  bj-0int  35251  bj-ismooredr  35259  bj-inftyexpiinj  35359  nlpfvineqsn  35559  wl-ax13lem1  35644  wl-speqv  35660  wl-sbcom2d  35695  wl-ax11-lem3  35717  wl-ax11-lem8  35722  tan2h  35748  ptrest  35755  poimirlem20  35776  poimirlem22  35778  poimirlem26  35782  poimirlem30  35786  poimirlem31  35787  poimirlem32  35788  heicant  35791  voliunnfl  35800  volsupnfl  35801  itg2addnclem2  35808  itg2addnc  35810  itg2gt0cn  35811  ftc2nc  35838  filbcmb  35877  sdclem2  35879  seqpo  35884  nninfnub  35888  neificl  35890  prdstotbnd  35931  cnpwstotbnd  35934  heibor1lem  35946  heibor  35958  bfplem2  35960  opidonOLD  35989  exidu1  35993  grpokerinj  36030  rngoideu  36040  rngodi  36041  rngodir  36042  rngmgmbs4  36068  divrngidl  36165  prnc  36204  eqvrelqsel  36708  erim2  36768  prter2  36874  ax4fromc4  36887  hbae-o  36896  dvelimf-o  36922  ax12indn  36936  ax12inda2  36940  ax12a2-o  36943  l1cvpat  37047  atcvrj0  37421  pmaple  37754  paddasslem5  37817  pclfinN  37893  osumcllem11N  37959  pexmidlem8N  37970  dvheveccl  39105  dihord6apre  39249  lpolconN  39480  lcmineqlem1  40017  oexpreposd  40301  sn-it0e0  40377  cnreeu  40418  isnacs3  40512  pellexlem5  40635  pellex  40637  jm2.18  40790  jm2.15nn0  40805  jm2.16nn0  40806  dford3lem2  40829  ttac  40838  rp-isfinite5  41086  cnvssb  41147  clcnvlem  41184  iunrelexpuztr  41280  rfovcnvf1od  41565  ntrrn  41685  nzss  41888  pm11.71  41968  axc11next  41977  hbntal  42126  eel2122old  42291  fsetsnf1  44497  2reu8i  44556  afvelima  44610  rlimdmafv  44620  rlimdmafv2  44701  elsprel  44879  sfprmdvdsmersenne  45007  perfectALTVlem2  45126  fpprwppr  45143  copisnmnd  45315  rnghmsscmap2  45483  rnghmsscmap  45484  rhmsscmap2  45529  rhmsscmap  45530  funcringcsetcALTV2lem8  45553  funcringcsetclem8ALTV  45576  lindslinindsimp2lem5  45755  nn0sumshdig  45921  prelrrx2b  46012  itscnhlc0yqe  46057  iscnrm3lem2  46180  spd  46336  setrec1lem4  46348  setrec2fun  46350  aacllem  46457