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  952  pm2.36  972  pm4.79  1006  ecased  1036  alrimdh  1865  stdpc5v  1940  19.37imv  1949  ax12w  2139  ax13dgen2  2144  ax12v  2186  spsd  2195  nf5r  2202  axc4  2327  equs5eALT  2372  ax13lem1  2379  nfeqf  2386  hbae  2436  ax12vALT  2474  2ax6elem  2475  sb1  2483  euimmo  2617  necon2ad  2948  necon4ad  2952  r19.37v  3164  spcimgfi1OLD  3494  rr19.28v  3611  moeq3  3659  reuimrmo  3692  sbeqalb  3792  replem  5223  csbexg  5245  ralxfrd  5345  ralxfrd2  5349  ralxfrALT  5352  copsexgw  5438  copsexg  5439  pwssun  5516  somo  5571  ssrel  5732  relssres  5981  dmsnopg  6171  dfco2a  6204  dfpo2  6254  frpoinsg  6301  tz7.7  6343  ordunidif  6367  suctr  6405  trsucss  6407  suc11  6426  imadif  6576  dffv2  6929  fvmptd3f  6957  fvmptnf  6964  foco2  7055  fconst5  7154  fvf1pr  7255  isores3  7283  riotaxfrd  7351  ovmpt4g  7507  ovmpos  7508  ov2gf  7509  ovmpodf  7516  sorpsscmpl  7681  abnexg  7703  onint  7737  limuni3  7796  tfisg  7798  tfis  7799  tfinds  7804  limomss  7815  peano5  7837  fo2ndf  8064  frxp  8069  xpord2pred  8088  xpord2indlem  8090  soseq  8102  suppss2  8143  suppssfv  8145  rntpos  8182  fprlem1  8243  fprresex  8253  wfr3g  8262  onfununi  8274  smofvon2  8289  smo11  8297  smoord  8298  tfrlem11  8320  tz7.44-2  8339  tz7.48lem  8373  tz7.48-1  8375  tz7.49  8377  tz7.49c  8378  omordi  8494  omord  8496  omass  8508  oneo  8509  omeulem1  8510  omopth2  8512  oewordri  8521  oeworde  8522  nnmordi  8560  nnmord  8561  omabs  8580  nnneo  8584  omsmo  8587  naddcllem  8605  qsel  8736  eceqoveq  8762  domunsncan  9008  sbthlem1  9018  2pwuninel  9063  mapen  9072  infensuc  9086  rexdif1en  9088  findcard2  9092  pssnn  9096  ssfi  9100  sucdom2  9130  php  9134  onomeneq  9141  0sdom1dom  9149  sdom1  9153  dif1ennnALT  9180  ac6sfi  9187  frfi  9188  unblem1  9195  unblem2  9196  unbnn2  9200  domunfican  9225  fodomfir  9231  ixpfi2  9253  finsschain  9262  unifi3  9265  marypha1lem  9339  oiexg  9443  brwdom3  9490  inf3lem2  9541  inf3lem3  9542  cantnfval2  9581  cantnflt  9584  cantnflem1  9601  cnfcom  9612  ttrclss  9632  trcl  9640  epfrs  9643  frmin  9664  frinsg  9666  frr3g  9671  frrlem15  9672  r1sdom  9689  cardsdomel  9889  carduni  9896  infpwfien  9975  carduniima  10009  dfac5  10042  dfac12r  10060  dfac12k  10061  kmlem11  10074  djuinf  10102  infxp  10127  cfsuc  10170  cfcoflem  10185  coftr  10186  infpssr  10221  fin23lem30  10255  isf32lem1  10266  isf34lem6  10293  fin1a2lem13  10325  fin1a2s  10327  axcc2lem  10349  domtriomlem  10355  axcclem  10370  ac6num  10392  zorn2lem5  10413  zorn2lem6  10414  axdclem2  10433  alephval2  10486  alephreg  10496  pwcfsdom  10497  axregndlem1  10516  axregnd  10518  axacndlem1  10521  axacndlem2  10522  axacndlem3  10523  axacndlem4  10524  axacnd  10526  gchi  10538  fpwwe2lem12  10556  canthp1  10568  gchpwdom  10584  wunfi  10635  tskwe2  10687  inar1  10689  gruen  10726  intgru  10728  indpi  10821  nqereu  10843  ltbtwnnq  10892  prnmadd  10911  genpcd  10920  prlem934  10947  ltexprlem1  10950  ltexprlem2  10951  ltexprlem7  10956  ltaprlem  10958  ltapr  10959  reclem4pr  10964  suplem2pr  10967  mulcmpblnr  10985  recexsrlem  11017  mulgt0sr  11019  supsrlem  11025  axpre-sup  11083  1re  11135  dedekindle  11301  addlsub  11557  recex  11773  nnunb  12424  0mnnnnn0  12460  prime  12601  zeo  12606  fnn0ind  12619  zindd  12621  btwnz  12623  lbzbi  12877  xrub  13255  elfznelfzo  13719  fvf1tp  13739  addmodlteq  13899  facwordi  14242  fiinfnf1o  14303  hashclb  14311  hashdom  14332  hashf1lem2  14409  seqcoll  14417  brfi1indALT  14463  ccatalpha  14547  pfxccatin12lem2a  14680  limsupbnd2  15436  rlimdm  15504  o1of2  15566  rlimno1  15607  isercoll  15621  caurcvg2  15631  caucvgb  15633  serf0  15634  zsum  15671  fsum2dlem  15723  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  zprod  15893  fprod2dlem  15936  fprod2d  15937  odd2np1  16301  ndvdssub  16369  dfgcd2  16506  nprm  16648  maxprmfct  16670  rpexp  16683  pc2dvds  16841  pcfac  16861  unbenlem  16870  4sqlem12  16918  4sqlem17  16923  vdwlem13  16955  prmlem0  17067  mreiincl  17549  sscfn1  17775  initoid  17959  termoid  17960  funcestrcsetclem8  18104  funcsetcestrclem8  18119  pospo  18300  cnvpsb  18536  dirtr  18559  mulgaddcom  19065  mulginvcom  19066  gaass  19263  cntz2ss  19301  elsymgbas  19340  symgfix2  19382  pmtrfrn  19424  psgnran  19481  odmulg  19522  odhash3  19542  sylow2alem1  19583  sylow2alem2  19584  pj1eu  19662  efgs1b  19702  efgsfo  19705  efgredlemc  19711  efgredeu  19718  frgpuptinv  19737  lt6abl  19861  ghmcyg  19862  ablfac1eulem  20040  pgpfac1lem5  20047  ablsimpgfindlem1  20075  gsumle  20111  ringinvnz1ne0  20272  irredmul  20400  rnghmsscmap2  20597  rnghmsscmap  20598  rhmsscmap2  20626  rhmsscmap  20627  acsfn1p  20767  lspextmo  21043  lspsncv0  21136  pzriprnglem12  21482  psgnghm  21570  mplcoe1  22025  mplcoe5  22028  evlseu  22071  mhpsclcl  22123  mdetunilem7  22593  mdetunilem9  22595  chcoeffeq  22861  cnindis  23267  lmss  23273  lmcls  23277  lmcnp  23279  hausnei  23303  cmpsub  23375  tgcmp  23376  fiuncmp  23379  cmpfi  23383  bwth  23385  1stcrest  23428  2ndcdisj  23431  1stccnp  23437  comppfsc  23507  1stckgenlem  23528  txcls  23579  txcn  23601  txlm  23623  tx1stc  23625  xkococn  23635  hmphdis  23771  ptcmpfi  23788  isfild  23833  fgss2  23849  filconn  23858  trfil2  23862  ufileu  23894  filufint  23895  elfm2  23923  flftg  23971  fclssscls  23993  fclscf  24000  ufilcmp  24007  cnpfcf  24016  alexsubb  24021  alexsubALTlem4  24025  alexsubALT  24026  qustgpopn  24095  tsmsxp  24130  isust  24179  xmettri2  24315  blin2  24404  setsmstopn  24453  met2ndc  24498  metcnp3  24515  tngtopn  24625  reconnlem2  24803  xrge0tsms  24810  fsumcn  24847  bndth  24935  iscmet3lem2  25269  iscmet3  25270  ivthlem1  25428  ivthlem2  25429  ivthlem3  25430  ovolfiniun  25478  volfiniun  25524  ioombl1lem4  25538  ismbf3d  25631  mbfi1flimlem  25699  itg2seq  25719  itgfsum  25804  ellimc3  25856  dvmptfsum  25952  c1liplem1  25973  plypf1  26187  plydivex  26274  aannenlem1  26305  ulmval  26358  ulmcau  26373  ulmbdd  26376  ulmcn  26377  ulmdvlem3  26380  sineq0  26501  efopn  26635  cxpeq  26734  logbgcd1irr  26771  rlimcnp  26942  xrlimcnp  26945  lgsdir2lem2  27303  lgsne0  27312  2lgsoddprm  27393  2sqlem6  27400  2sqlem10  27405  2sqreunnltblem  27428  ltsval2  27634  noetasuplem4  27714  conway  27785  madebdayim  27894  addsass  28011  oncutlt  28270  oniso  28277  addonbday  28285  n0ssoldg  28359  bdayn0p1  28375  oldfib  28383  bdaypw2n0bndlem  28469  bdayfinbndlem1  28473  z12bdaylem1  28476  z12zsodd  28488  axcontlem2  29048  uhgr0vb  29155  uvtx01vtx  29480  uvtxupgrres  29491  fusgrn0degnn0  29583  finsumvtxdg2size  29634  cusgrm1rusgr  29666  wlkv0  29733  wlklenvclwlk  29737  uspgrn2crct  29891  frrusgrord  30426  numclwwlk1lem2fo  30443  isgrpo  30583  grpoidinvlem3  30592  vcdi  30651  vcdir  30652  vcass  30653  nvs  30749  nvtri  30756  blocnilem  30890  chintcli  31417  hsupss  31427  shlej1  31446  elspansn4  31659  spansncvi  31738  hoaddsub  31902  lnopl  32000  lnfnl  32017  riesz4i  32149  pjnormssi  32254  pj3si  32293  stlei  32326  stcltr2i  32361  dmdmd  32386  dmdbr5  32394  mdslmd1lem2  32412  atssma  32464  atcvatlem  32471  chirredlem1  32476  atcvat4i  32483  mdsymlem2  32490  mdsymlem6  32494  sumdmdlem2  32505  cdjreui  32518  elimifd  32628  disjxpin  32673  xrge0infss  32848  expgt0b  32905  xrge0tsmsd  33149  gsumvsca1  33302  gsumvsca2  33303  lmxrge0  34112  ismeas  34359  eulerpartlemb  34528  bnj849  35083  bnj1110  35140  srcmpltd  35238  axprALT2  35269  trssfir1om  35271  fineqvinfep  35285  trssfir1omregs  35296  swrdrevpfx  35315  cusgredgex2  35321  subgrwlk  35330  cusgr3cyclex  35334  umgr2cycllem  35338  umgr2cycl  35339  connpconn  35433  cvmseu  35474  cvmliftlem15  35496  cvmlift2lem1  35500  cvmlift2lem12  35512  satfv0fun  35569  satffunlem  35599  mclsind  35768  r1peuqusdeg1  35841  dfon2lem3  35981  dfon2lem4  35982  dfon2lem6  35984  dfon2lem8  35986  dfon2lem9  35987  hbntg  36001  cgrdegen  36202  funtransport  36229  ifscgr  36242  cgrxfr  36253  brofs2  36275  brifs2  36276  idinside  36282  btwnconn1lem7  36291  btwnconn1lem11  36295  btwnconn1lem12  36296  btwnconn1lem14  36298  broutsideof2  36320  btwnoutside  36323  outsideoftr  36327  in-ax8  36422  ss-ax8  36423  finminlem  36516  ntruni  36525  neibastop1  36557  ontgval  36629  ordtop  36634  ordcmp  36645  onint1  36647  bj-alrimdh  36905  bj-spimnfe  36934  bj-spimenfa  36935  bj-cbveximd  36942  bj-spvew  36946  bj-cbvexvv  36950  bj-ax12w  36988  axc11n11r  36996  bj-ax12v3  36998  bj-nnfan  37067  bj-nnfand  37068  bj-19.42t  37078  bj-sbft  37091  bj-nnflemea  37102  bj-hbaeb2  37141  bj-spcimdv  37218  bj-spcimdvv  37219  bj-sngltag  37306  bj-xtagex  37312  bj-axseprep  37397  bj-0int  37429  bj-ismooredr  37437  bj-inftyexpiinj  37539  nlpfvineqsn  37739  wl-ax13lem1  37824  wl-speqv  37861  wl-sbcom2d  37900  tan2h  37947  ptrest  37954  poimirlem20  37975  poimirlem22  37977  poimirlem26  37981  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  heicant  37990  voliunnfl  37999  volsupnfl  38000  itg2addnclem2  38007  itg2addnc  38009  itg2gt0cn  38010  ftc2nc  38037  filbcmb  38075  sdclem2  38077  seqpo  38082  nninfnub  38086  neificl  38088  prdstotbnd  38129  cnpwstotbnd  38132  heibor1lem  38144  heibor  38156  bfplem2  38158  opidonOLD  38187  exidu1  38191  grpokerinj  38228  rngoideu  38238  rngodi  38239  rngodir  38240  rngmgmbs4  38266  divrngidl  38363  prnc  38402  rsp3eq  38702  eqvrelqsel  39035  erimeq2  39098  prter2  39341  ax4fromc4  39354  hbae-o  39363  dvelimf-o  39389  ax12indn  39403  ax12inda2  39407  ax12a2-o  39410  l1cvpat  39514  atcvrj0  39888  pmaple  40221  paddasslem5  40284  pclfinN  40360  osumcllem11N  40426  pexmidlem8N  40437  dvheveccl  41572  dihord6apre  41716  lpolconN  41947  lcmineqlem1  42482  oexpreposd  42768  sn-it0e0  42862  cnreeu  42949  eu6w  43123  isnacs3  43156  pellexlem5  43279  pellex  43281  jm2.18  43434  jm2.15nn0  43449  jm2.16nn0  43450  dford3lem2  43473  ttac  43482  onexomgt  43687  onexoegt  43690  omabs2  43778  omcl3g  43780  tfsconcat0b  43792  naddgeoa  43840  safesnsupfiss  43860  rp-isfinite5  43962  cnvssb  44031  clcnvlem  44068  iunrelexpuztr  44164  rfovcnvf1od  44449  ntrrn  44567  nzss  44762  pm11.71  44842  axc11next  44851  hbntal  44998  eel2122old  45162  relwf  45412  modelaxreplem1  45423  ssclaxsep  45427  wfac8prim  45447  fsetsnf1  47512  2reu8i  47573  afvelima  47627  rlimdmafv  47637  rlimdmafv2  47718  elsprel  47947  sfprmdvdsmersenne  48078  perfectALTVlem2  48210  fpprwppr  48227  uhgrimedgi  48378  isuspgrim0lem  48381  uhgrimisgrgric  48419  gpgcubic  48567  gpg5nbgr3star  48569  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  copisnmnd  48657  funcringcsetcALTV2lem8  48785  funcringcsetclem8ALTV  48808  lindslinindsimp2lem5  48950  nn0sumshdig  49111  prelrrx2b  49202  itscnhlc0yqe  49247  iscnrm3lem2  49422  diag1f1lem  49793  spd  50165  setrec1lem4  50177  setrec2fun  50179  aacllem  50288