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  1864  stdpc5v  1939  19.37imv  1948  ax12w  2138  ax13dgen2  2143  ax12v  2185  spsd  2194  nf5r  2201  axc4  2326  equs5eALT  2371  ax13lem1  2378  nfeqf  2385  hbae  2435  ax12vALT  2473  2ax6elem  2474  sb1  2482  euimmo  2616  necon2ad  2947  necon4ad  2951  r19.37v  3162  spcimgfi1OLD  3505  rr19.28v  3622  moeq3  3670  reuimrmo  3703  sbeqalb  3803  csbexg  5255  ralxfrd  5353  ralxfrd2  5357  ralxfrALT  5360  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  6956  fvmptnf  6963  foco2  7054  fconst5  7152  fvf1pr  7253  isores3  7281  riotaxfrd  7349  ovmpt4g  7505  ovmpos  7506  ov2gf  7507  ovmpodf  7514  sorpsscmpl  7679  abnexg  7701  onint  7735  limuni3  7794  tfisg  7796  tfis  7797  tfinds  7802  limomss  7813  peano5  7835  fo2ndf  8063  frxp  8068  xpord2pred  8087  xpord2indlem  8089  soseq  8101  suppss2  8142  suppssfv  8144  rntpos  8181  fprlem1  8242  fprresex  8252  wfr3g  8261  onfununi  8273  smofvon2  8288  smo11  8296  smoord  8297  tfrlem11  8319  tz7.44-2  8338  tz7.48lem  8372  tz7.48-1  8374  tz7.49  8376  tz7.49c  8377  omordi  8493  omord  8495  omass  8507  oneo  8508  omeulem1  8509  omopth2  8511  oewordri  8520  oeworde  8521  nnmordi  8559  nnmord  8560  omabs  8579  nnneo  8583  omsmo  8586  naddcllem  8604  qsel  8733  eceqoveq  8759  domunsncan  9005  sbthlem1  9015  2pwuninel  9060  mapen  9069  infensuc  9083  rexdif1en  9085  findcard2  9089  pssnn  9093  ssfi  9097  sucdom2  9127  php  9131  onomeneq  9138  0sdom1dom  9146  sdom1  9150  dif1ennnALT  9177  ac6sfi  9184  frfi  9185  unblem1  9192  unblem2  9193  unbnn2  9197  domunfican  9222  fodomfir  9228  ixpfi2  9250  finsschain  9259  unifi3  9262  marypha1lem  9336  oiexg  9440  brwdom3  9487  inf3lem2  9538  inf3lem3  9539  cantnfval2  9578  cantnflt  9581  cantnflem1  9598  cnfcom  9609  ttrclss  9629  trcl  9637  epfrs  9640  frmin  9661  frinsg  9663  frr3g  9668  frrlem15  9669  r1sdom  9686  cardsdomel  9886  carduni  9893  infpwfien  9972  carduniima  10006  dfac5  10039  dfac12r  10057  dfac12k  10058  kmlem11  10071  djuinf  10099  infxp  10124  cfsuc  10167  cfcoflem  10182  coftr  10183  infpssr  10218  fin23lem30  10252  isf32lem1  10263  isf34lem6  10290  fin1a2lem13  10322  fin1a2s  10324  axcc2lem  10346  domtriomlem  10352  axcclem  10367  ac6num  10389  zorn2lem5  10410  zorn2lem6  10411  axdclem2  10430  alephval2  10483  alephreg  10493  pwcfsdom  10494  axregndlem1  10513  axregnd  10515  axacndlem1  10518  axacndlem2  10519  axacndlem3  10520  axacndlem4  10521  axacnd  10523  gchi  10535  fpwwe2lem12  10553  canthp1  10565  gchpwdom  10581  wunfi  10632  tskwe2  10684  inar1  10686  gruen  10723  intgru  10725  indpi  10818  nqereu  10840  ltbtwnnq  10889  prnmadd  10908  genpcd  10917  prlem934  10944  ltexprlem1  10947  ltexprlem2  10948  ltexprlem7  10953  ltaprlem  10955  ltapr  10956  reclem4pr  10961  suplem2pr  10964  mulcmpblnr  10982  recexsrlem  11014  mulgt0sr  11016  supsrlem  11022  axpre-sup  11080  1re  11132  dedekindle  11297  addlsub  11553  recex  11769  nnunb  12397  0mnnnnn0  12433  prime  12573  zeo  12578  fnn0ind  12591  zindd  12593  btwnz  12595  lbzbi  12849  xrub  13227  elfznelfzo  13689  fvf1tp  13709  addmodlteq  13869  facwordi  14212  fiinfnf1o  14273  hashclb  14281  hashdom  14302  hashf1lem2  14379  seqcoll  14387  brfi1indALT  14433  ccatalpha  14517  pfxccatin12lem2a  14650  limsupbnd2  15406  rlimdm  15474  o1of2  15536  rlimno1  15577  isercoll  15591  caurcvg2  15601  caucvgb  15603  serf0  15604  zsum  15641  fsum2dlem  15693  fsum2d  15694  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  zprod  15860  fprod2dlem  15903  fprod2d  15904  odd2np1  16268  ndvdssub  16336  dfgcd2  16473  nprm  16615  maxprmfct  16636  rpexp  16649  pc2dvds  16807  pcfac  16827  unbenlem  16836  4sqlem12  16884  4sqlem17  16889  vdwlem13  16921  prmlem0  17033  mreiincl  17515  sscfn1  17741  initoid  17925  termoid  17926  funcestrcsetclem8  18070  funcsetcestrclem8  18085  pospo  18266  cnvpsb  18502  dirtr  18525  mulgaddcom  19028  mulginvcom  19029  gaass  19226  cntz2ss  19264  elsymgbas  19303  symgfix2  19345  pmtrfrn  19387  psgnran  19444  odmulg  19485  odhash3  19505  sylow2alem1  19546  sylow2alem2  19547  pj1eu  19625  efgs1b  19665  efgsfo  19668  efgredlemc  19674  efgredeu  19681  frgpuptinv  19700  lt6abl  19824  ghmcyg  19825  ablfac1eulem  20003  pgpfac1lem5  20010  ablsimpgfindlem1  20038  gsumle  20074  ringinvnz1ne0  20235  irredmul  20365  rnghmsscmap2  20562  rnghmsscmap  20563  rhmsscmap2  20591  rhmsscmap  20592  acsfn1p  20732  lspextmo  21008  lspsncv0  21101  pzriprnglem12  21447  psgnghm  21535  mplcoe1  21992  mplcoe5  21995  evlseu  22038  mhpsclcl  22090  mdetunilem7  22562  mdetunilem9  22564  chcoeffeq  22830  cnindis  23236  lmss  23242  lmcls  23246  lmcnp  23248  hausnei  23272  cmpsub  23344  tgcmp  23345  fiuncmp  23348  cmpfi  23352  bwth  23354  1stcrest  23397  2ndcdisj  23400  1stccnp  23406  comppfsc  23476  1stckgenlem  23497  txcls  23548  txcn  23570  txlm  23592  tx1stc  23594  xkococn  23604  hmphdis  23740  ptcmpfi  23757  isfild  23802  fgss2  23818  filconn  23827  trfil2  23831  ufileu  23863  filufint  23864  elfm2  23892  flftg  23940  fclssscls  23962  fclscf  23969  ufilcmp  23976  cnpfcf  23985  alexsubb  23990  alexsubALTlem4  23994  alexsubALT  23995  qustgpopn  24064  tsmsxp  24099  isust  24148  xmettri2  24284  blin2  24373  setsmstopn  24422  met2ndc  24467  metcnp3  24484  tngtopn  24594  reconnlem2  24772  xrge0tsms  24779  fsumcn  24817  bndth  24913  iscmet3lem2  25248  iscmet3  25249  ivthlem1  25408  ivthlem2  25409  ivthlem3  25410  ovolfiniun  25458  volfiniun  25504  ioombl1lem4  25518  ismbf3d  25611  mbfi1flimlem  25679  itg2seq  25699  itgfsum  25784  ellimc3  25836  dvmptfsum  25935  c1liplem1  25957  plypf1  26173  plydivex  26261  aannenlem1  26292  ulmval  26345  ulmcau  26360  ulmbdd  26363  ulmcn  26364  ulmdvlem3  26367  sineq0  26489  efopn  26623  cxpeq  26723  logbgcd1irr  26760  rlimcnp  26931  xrlimcnp  26934  lgsdir2lem2  27293  lgsne0  27302  2lgsoddprm  27383  2sqlem6  27390  2sqlem10  27395  2sqreunnltblem  27418  ltsval2  27624  noetasuplem4  27704  conway  27775  madebdayim  27884  addsass  28001  oncutlt  28260  oniso  28267  addonbday  28275  n0ssoldg  28349  bdayn0p1  28365  oldfib  28373  bdaypw2n0bndlem  28459  bdayfinbndlem1  28463  z12bdaylem1  28466  z12zsodd  28478  axcontlem2  29038  uhgr0vb  29145  uvtx01vtx  29470  uvtxupgrres  29481  fusgrn0degnn0  29573  finsumvtxdg2size  29624  cusgrm1rusgr  29656  wlkv0  29723  wlklenvclwlk  29727  uspgrn2crct  29881  frrusgrord  30416  numclwwlk1lem2fo  30433  isgrpo  30572  grpoidinvlem3  30581  vcdi  30640  vcdir  30641  vcass  30642  nvs  30738  nvtri  30745  blocnilem  30879  chintcli  31406  hsupss  31416  shlej1  31435  elspansn4  31648  spansncvi  31727  hoaddsub  31891  lnopl  31989  lnfnl  32006  riesz4i  32138  pjnormssi  32243  pj3si  32282  stlei  32315  stcltr2i  32350  dmdmd  32375  dmdbr5  32383  mdslmd1lem2  32401  atssma  32453  atcvatlem  32460  chirredlem1  32465  atcvat4i  32472  mdsymlem2  32479  mdsymlem6  32483  sumdmdlem2  32494  cdjreui  32507  elimifd  32618  disjxpin  32663  xrge0infss  32840  expgt0b  32897  xrge0tsmsd  33155  gsumvsca1  33308  gsumvsca2  33309  lmxrge0  34109  ismeas  34356  eulerpartlemb  34525  bnj849  35081  bnj1110  35138  srcmpltd  35236  trssfir1om  35267  fineqvinfep  35281  trssfir1omregs  35292  swrdrevpfx  35311  cusgredgex2  35317  subgrwlk  35326  cusgr3cyclex  35330  umgr2cycllem  35334  umgr2cycl  35335  connpconn  35429  cvmseu  35470  cvmliftlem15  35492  cvmlift2lem1  35496  cvmlift2lem12  35508  satfv0fun  35565  satffunlem  35595  mclsind  35764  r1peuqusdeg1  35837  dfon2lem3  35977  dfon2lem4  35978  dfon2lem6  35980  dfon2lem8  35982  dfon2lem9  35983  hbntg  35997  cgrdegen  36198  funtransport  36225  ifscgr  36238  cgrxfr  36249  brofs2  36271  brifs2  36272  idinside  36278  btwnconn1lem7  36287  btwnconn1lem11  36291  btwnconn1lem12  36292  btwnconn1lem14  36294  broutsideof2  36316  btwnoutside  36319  outsideoftr  36323  in-ax8  36418  ss-ax8  36419  finminlem  36512  ntruni  36521  neibastop1  36553  ontgval  36625  ordtop  36630  ordcmp  36641  onint1  36643  bj-ax12w  36878  axc11n11r  36884  bj-ax12v3  36886  bj-nnfan  36949  bj-nnfand  36950  bj-nnflemea  36966  bj-19.42t  36974  bj-sbft  36976  bj-hbaeb2  37019  bj-spcimdv  37096  bj-spcimdvv  37097  bj-sngltag  37184  bj-xtagex  37190  bj-0int  37302  bj-ismooredr  37310  bj-inftyexpiinj  37410  nlpfvineqsn  37610  wl-ax13lem1  37695  wl-speqv  37723  wl-sbcom2d  37762  tan2h  37809  ptrest  37816  poimirlem20  37837  poimirlem22  37839  poimirlem26  37843  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  heicant  37852  voliunnfl  37861  volsupnfl  37862  itg2addnclem2  37869  itg2addnc  37871  itg2gt0cn  37872  ftc2nc  37899  filbcmb  37937  sdclem2  37939  seqpo  37944  nninfnub  37948  neificl  37950  prdstotbnd  37991  cnpwstotbnd  37994  heibor1lem  38006  heibor  38018  bfplem2  38020  opidonOLD  38049  exidu1  38053  grpokerinj  38090  rngoideu  38100  rngodi  38101  rngodir  38102  rngmgmbs4  38128  divrngidl  38225  prnc  38264  eqvrelqsel  38869  erimeq2  38933  prter2  39137  ax4fromc4  39150  hbae-o  39159  dvelimf-o  39185  ax12indn  39199  ax12inda2  39203  ax12a2-o  39206  l1cvpat  39310  atcvrj0  39684  pmaple  40017  paddasslem5  40080  pclfinN  40156  osumcllem11N  40222  pexmidlem8N  40233  dvheveccl  41368  dihord6apre  41512  lpolconN  41743  lcmineqlem1  42279  oexpreposd  42573  sn-it0e0  42667  cnreeu  42741  eu6w  42915  isnacs3  42948  pellexlem5  43071  pellex  43073  jm2.18  43226  jm2.15nn0  43241  jm2.16nn0  43242  dford3lem2  43265  ttac  43274  onexomgt  43479  onexoegt  43482  omabs2  43570  omcl3g  43572  tfsconcat0b  43584  naddgeoa  43632  safesnsupfiss  43652  rp-isfinite5  43754  cnvssb  43823  clcnvlem  43860  iunrelexpuztr  43956  rfovcnvf1od  44241  ntrrn  44359  nzss  44554  pm11.71  44634  axc11next  44643  hbntal  44790  eel2122old  44954  relwf  45204  modelaxreplem1  45215  ssclaxsep  45219  wfac8prim  45239  fsetsnf1  47294  2reu8i  47355  afvelima  47409  rlimdmafv  47419  rlimdmafv2  47500  elsprel  47717  sfprmdvdsmersenne  47845  perfectALTVlem2  47964  fpprwppr  47981  uhgrimedgi  48132  isuspgrim0lem  48135  uhgrimisgrgric  48173  gpgcubic  48321  gpg5nbgr3star  48323  pgnioedg1  48350  pgnioedg2  48351  pgnioedg3  48352  pgnioedg4  48353  pgnioedg5  48354  copisnmnd  48411  funcringcsetcALTV2lem8  48539  funcringcsetclem8ALTV  48562  lindslinindsimp2lem5  48704  nn0sumshdig  48865  prelrrx2b  48956  itscnhlc0yqe  49001  iscnrm3lem2  49176  diag1f1lem  49547  spd  49919  setrec1lem4  49931  setrec2fun  49933  aacllem  50042