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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl56  37  syl2im  41  imim12i  63  pm2.86d  109  con2d  135  con3d  153  nsyli  158  biimtrid  245  biimtrrid  246  imbitrid  247  adantld  496  adantrd  497  impel  515  mpan9  516  pm4.72  964  pm2.36  985  pm4.79  1021  ecased  1051  alrimdh  1896  stdpc5v  1971  19.37imv  1980  ax12w  2171  ax13dgen2  2176  ax12v  2217  spsd  2226  nf5r  2233  axc4  2357  equs5eALT  2402  ax13lem1  2409  nfeqf  2416  hbae  2466  ax12vALT  2504  2ax6elem  2505  sb1  2513  euimmo  2647  necon2ad  2976  necon4ad  2980  r19.37v  3194  rr19.28v  3630  moeq3  3678  reuimrmo  3711  sbeqalb  3809  srcmpltd  4442  replem  5254  csbexg  5278  ralxfrd  5384  ralxfrd2  5388  ralxfrALT  5391  copsexgwOLD  5478  copsexg  5479  pwssun  5558  somo  5613  ssrel  5774  relssres  6026  dmsnopg  6219  dfco2a  6252  dfpo2  6304  frpoinsg  6351  tz7.7  6393  ordunidif  6418  suctr  6456  trsucss  6458  suc11  6477  imadif  6627  dffv2  6983  fvmptd3f  7012  fvmptnf  7019  foco2  7111  fconst5  7211  fvf1pr  7316  isores3  7344  riotaxfrd  7414  ovmpt4g  7570  ovmpos  7571  ov2gf  7572  ovmpodf  7579  sorpsscmpl  7744  abnexg  7764  onint  7798  limuni3  7857  tfisg  7859  tfis  7860  tfinds  7865  limomss  7876  peano5  7899  fo2ndf  8125  frxp  8131  xpord2pred  8150  xpord2indlem  8152  soseq  8164  suppss2  8205  suppssfv  8207  rntpos  8244  fprlem1  8306  fprresex  8316  wfr3g  8325  onfununi  8337  smofvon2  8352  smo11  8360  smoord  8361  tfrlem11  8384  tz7.44-2  8403  tz7.48lem  8437  tz7.48-1  8439  tz7.49  8441  tz7.49c  8442  omordi  8560  omord  8562  omass  8574  oneo  8575  omeulem1  8576  omopth2  8578  oewordri  8587  oeworde  8588  nnmordi  8626  nnmord  8627  omabs  8646  nnneo  8650  omsmo  8653  naddcllem  8671  qsel  8803  eceqoveq  8829  domunsncan  9075  sbthlem1  9085  2pwuninel  9130  mapen  9139  infensuc  9153  rexdif1en  9155  findcard2  9159  pssnn  9163  ssfi  9167  sucdom2  9197  php  9201  onomeneq  9208  0sdom1dom  9216  sdom1  9220  dif1ennnALT  9247  ac6sfi  9254  frfi  9255  unblem1  9262  unblem2  9263  unbnn2  9267  domunfican  9291  fodomfir  9297  ixpfi2  9317  finsschain  9326  unifi3  9329  marypha1lem  9403  oiexg  9507  brwdom3  9554  inf3lem2  9608  inf3lem3  9609  cantnfval2  9648  cantnflt  9651  cantnflem1  9668  cnfcom  9679  ttrclss  9699  trcl  9707  epfrs  9710  frmin  9731  frinsg  9733  frr3g  9738  frrlem15  9739  r1sdom  9756  cardsdomel  9979  carduni  9986  infpwfien  10065  carduniima  10099  dfac5  10131  dfac12r  10149  dfac12k  10150  kmlem11  10163  djuinf  10191  infxp  10216  cfsuc  10259  cfcoflem  10274  coftr  10275  infpssr  10310  fin23lem30  10344  isf32lem1  10355  isf34lem6  10382  fin1a2lem13  10414  fin1a2s  10416  axcc2lem  10438  domtriomlem  10444  axcclem  10459  ac6num  10481  zorn2lem5  10502  zorn2lem6  10503  axdclem2  10522  alephval2  10575  alephreg  10585  pwcfsdom  10586  axregndlem1  10605  axregnd  10607  axacndlem1  10610  axacndlem2  10611  axacndlem3  10612  axacndlem4  10613  axacnd  10615  gchi  10627  fpwwe2lem12  10645  canthp1  10657  gchpwdom  10673  wunfi  10724  tskwe2  10776  inar1  10778  gruen  10815  intgru  10817  indpi  10910  nqereu  10932  ltbtwnnq  10981  prnmadd  11000  genpcd  11009  prlem934  11036  ltexprlem1  11039  ltexprlem2  11040  ltexprlem7  11045  ltaprlem  11047  ltapr  11048  reclem4pr  11053  suplem2pr  11056  mulcmpblnr  11074  recexsrlem  11106  mulgt0sr  11108  supsrlem  11114  axpre-sup  11172  1re  11226  dedekindle  11392  addlsub  11648  recex  11864  nnunb  12518  0mnnnnn0  12554  prime  12695  zeo  12700  fnn0ind  12713  zindd  12715  btwnz  12717  lbzbi  12978  xrub  13356  elfznelfzo  13821  fvf1tp  13842  addmodlteq  14002  facwordi  14345  fiinfnf1o  14406  hashclb  14414  hashdom  14435  hashf1lem2  14513  seqcoll  14521  brfi1indALT  14567  ccatalpha  14652  pfxccatin12lem2a  14788  swrdrevpfx  14830  limsupbnd2  15560  rlimdm  15628  o1of2  15690  rlimno1  15731  isercoll  15745  caurcvg2  15755  caucvgb  15757  serf0  15758  zsum  15795  fsum2dlem  15847  fsum2d  15848  fsumabs  15879  fsumrlim  15889  fsumo1  15890  fsumiun  15899  zprod  16017  fprod2dlem  16060  fprod2d  16061  odd2np1  16424  ndvdssub  16492  dfgcd2  16629  nprm  16771  maxprmfct  16793  rpexp  16806  pc2dvds  16964  pcfac  16984  unbenlem  16993  4sqlem12  17041  4sqlem17  17046  vdwlem13  17078  prmlem0  17190  mreiincl  17673  sscfn1  17899  initoid  18083  termoid  18084  funcestrcsetclem8  18228  funcsetcestrclem8  18243  pospo  18424  cnvpsb  18660  dirtr  18683  mulgaddcom  19195  mulginvcom  19196  gaass  19398  cntz2ss  19436  elsymgbas  19475  symgfix2  19517  pmtrfrn  19559  psgnran  19616  odmulg  19657  odhash3  19677  sylow2alem1  19718  sylow2alem2  19719  pj1eu  19797  efgs1b  19837  efgsfo  19840  efgredlemc  19846  efgredeu  19853  frgpuptinv  19872  lt6abl  19996  ghmcyg  19997  ablfac1eulem  20175  pgpfac1lem5  20182  ablsimpgfindlem1  20210  gsumle  20246  ringinvnz1ne0  20416  irredmul  20544  rnghmsscmap2  20765  rnghmsscmap  20766  rhmsscmap2  20794  rhmsscmap  20795  acsfn1p  20939  lspextmo  21214  lspsncv0  21307  pzriprnglem12  21679  psgnghm  21767  mplcoe1  22225  mplcoe5  22228  evlseu  22271  mhpsclcl  22347  mdetunilem7  22812  mdetunilem9  22814  chcoeffeq  23080  cnindis  23486  lmss  23492  lmcls  23496  lmcnp  23498  hausnei  23522  cmpsub  23594  tgcmp  23595  fiuncmp  23598  cmpfi  23602  bwth  23604  1stcrest  23647  2ndcdisj  23650  1stccnp  23656  comppfsc  23726  1stckgenlem  23747  txcls  23798  txcn  23820  txlm  23842  tx1stc  23844  xkococn  23854  hmphdis  23990  ptcmpfi  24007  isfild  24052  fgss2  24068  filconn  24077  trfil2  24081  ufileu  24113  filufint  24114  elfm2  24142  flftg  24190  fclssscls  24212  fclscf  24219  ufilcmp  24226  cnpfcf  24235  alexsubb  24240  alexsubALTlem4  24244  alexsubALT  24245  qustgpopn  24314  tsmsxp  24349  isust  24398  xmettri2  24534  blin2  24623  setsmstopn  24672  met2ndc  24717  metcnp3  24734  tngtopn  24844  reconnlem2  25022  xrge0tsms  25029  fsumcn  25066  bndth  25154  iscmet3lem2  25488  iscmet3  25489  ivthlem1  25647  ivthlem2  25648  ivthlem3  25649  ovolfiniun  25697  volfiniun  25743  ioombl1lem4  25757  ismbf3d  25850  mbfi1flimlem  25918  itg2seq  25938  itgfsum  26023  ellimc3  26075  dvmptfsum  26171  c1liplem1  26192  plypf1  26406  plydivex  26495  aannenlem1  26528  ulmval  26580  ulmcau  26595  ulmbdd  26598  ulmcn  26599  ulmdvlem3  26602  sineq0  26726  efopn  26860  cxpeq  26959  logbgcd1irr  26996  rlimcnp  27167  xrlimcnp  27170  lgsdir2lem2  27527  lgsne0  27536  2lgsoddprm  27617  2sqlem6  27624  2sqlem10  27629  2sqreunnltblem  27652  ltsval2  27857  noetasuplem4  27937  conway  28009  madebdayim  28118  addsass  28235  oncutlt  28494  oniso  28501  addonbday  28509  n0ssoldg  28583  bdayn0p1  28599  oldfib  28607  bdaypw2n0bndlem  28693  bdayfinbndlem1  28697  z12bdaylem1  28700  z12zsodd  28712  axcontlem2  29352  uhgr0vb  29459  uvtx01vtx  29784  uvtxupgrres  29795  fusgrn0degnn0  29886  finsumvtxdg2size  29937  cusgrm1rusgr  29969  wlkv0  30036  wlklenvclwlk  30040  uspgrn2crct  30194  frrusgrord  30729  numclwwlk1lem2fo  30746  isgrpo  30886  grpoidinvlem3  30895  vcdi  30954  vcdir  30955  vcass  30956  nvs  31052  nvtri  31059  blocnilem  31193  chintcli  31720  hsupss  31730  shlej1  31749  elspansn4  31962  spansncvi  32041  hoaddsub  32205  lnopl  32303  lnfnl  32320  riesz4i  32452  pjnormssi  32557  pj3si  32596  stlei  32629  stcltr2i  32664  dmdmd  32689  dmdbr5  32697  mdslmd1lem2  32715  atssma  32767  atcvatlem  32774  chirredlem1  32779  atcvat4i  32786  mdsymlem2  32793  mdsymlem6  32797  sumdmdlem2  32808  cdjreui  32821  elimifd  32926  disjxpin  32970  xrge0infss  33142  expgt0b  33198  xrge0tsmsd  33424  gsumvsca1  33577  gsumvsca2  33578  lmxrge0  34373  ismeas  34621  eulerpartlemb  34790  bnj849  35345  bnj1110  35402  axprALT2  35528  trssfir1om  35532  fineqvinfep  35562  trssfir1omregs  35573  cusgredgex2  35636  subgrwlk  35645  cusgr3cyclex  35649  umgr2cycllem  35653  umgr2cycl  35654  connpconn  35748  cvmseu  35789  cvmliftlem15  35811  cvmlift2lem1  35815  cvmlift2lem12  35827  satfv0fun  35884  satffunlem  35914  mclsind  36083  r1peuqusdeg1  36156  dfon2lem3  36296  dfon2lem4  36297  dfon2lem6  36299  dfon2lem8  36301  dfon2lem9  36302  hbntg  36316  cgrdegen  36517  funtransport  36544  ifscgr  36557  cgrxfr  36568  brofs2  36590  brifs2  36591  idinside  36597  btwnconn1lem7  36606  btwnconn1lem11  36610  btwnconn1lem12  36611  btwnconn1lem14  36613  broutsideof2  36635  btwnoutside  36638  outsideoftr  36642  nmulprop  36703  in-ax8  36777  ss-ax8  36778  finminlem  36870  ntruni  36879  neibastop1  36911  ontgval  36983  ordtop  36988  ordcmp  36999  onint1  37001  bj-alrimdh  37258  bj-spimnfe  37287  bj-spimenfa  37288  bj-cbveximd  37295  bj-spvew  37299  bj-cbvexvv  37303  bj-ax12w  37341  axc11n11r  37349  bj-ax12v3  37351  bj-nnfan  37420  bj-nnfand  37421  bj-19.42t  37431  bj-sbft  37444  bj-nnflemea  37455  bj-hbaeb2  37494  bj-spcimdv  37571  bj-spcimdvv  37572  bj-sngltag  37660  bj-xtagex  37666  bj-axseprep  37752  bj-0int  37784  bj-ismooredr  37792  bj-inftyexpiinj  37894  nlpfvineqsn  38096  wl-ax13lem1  38181  wl-speqv  38218  wl-sbcom2d  38257  tan2h  38304  ptrest  38311  poimirlem20  38332  poimirlem22  38334  poimirlem26  38338  poimirlem30  38342  poimirlem31  38343  poimirlem32  38344  heicant  38347  voliunnfl  38356  volsupnfl  38357  itg2addnclem2  38364  itg2addnc  38366  itg2gt0cn  38367  ftc2nc  38394  filbcmb  38432  sdclem2  38434  seqpo  38439  nninfnub  38443  neificl  38445  prdstotbnd  38486  cnpwstotbnd  38489  heibor1lem  38501  heibor  38513  bfplem2  38515  opidonOLD  38544  exidu1  38548  grpokerinj  38585  rngoideu  38595  rngodi  38596  rngodir  38597  rngmgmbs4  38623  divrngidl  38720  prnc  38759  rsp3eq  39057  eqvrelqsel  39390  erimeq2  39453  prter2  39696  ax4fromc4  39709  hbae-o  39718  dvelimf-o  39744  ax12indn  39758  ax12inda2  39762  ax12a2-o  39765  l1cvpat  39869  atcvrj0  40243  pmaple  40576  paddasslem5  40639  pclfinN  40715  osumcllem11N  40781  pexmidlem8N  40792  dvheveccl  41927  dihord6apre  42071  lpolconN  42302  lcmineqlem1  42837  oexpreposd  43124  sn-it0e0  43218  cnreeu  43305  eu6w  43449  isnacs3  43482  pellexlem5  43601  pellex  43603  jm2.18  43756  jm2.15nn0  43771  jm2.16nn0  43772  dford3lem2  43795  ttac  43804  onexomgt  44009  onexoegt  44012  omabs2  44100  omcl3g  44102  tfsconcat0b  44114  naddgeoa  44162  safesnsupfiss  44182  rp-isfinite5  44284  cnvssb  44353  clcnvlem  44390  iunrelexpuztr  44486  rfovcnvf1od  44771  ntrrn  44889  nzss  45068  pm11.71  45148  axc11next  45157  hbntal  45303  eel2122old  45467  relwf  45717  modelaxreplem1  45728  ssclaxsep  45732  wfac8prim  45752  fsetsnf1  47830  2reu8i  47891  afvelima  47945  rlimdmafv  47955  rlimdmafv2  48036  elsprel  48265  sfprmdvdsmersenne  48396  perfectALTVlem2  48528  fpprwppr  48545  uhgrimedgi  48696  isuspgrim0lem  48699  uhgrimisgrgric  48737  gpgcubic  48885  gpg5nbgr3star  48887  pgnioedg1  48914  pgnioedg2  48915  pgnioedg3  48916  pgnioedg4  48917  pgnioedg5  48918  copisnmnd  48975  funcringcsetcALTV2lem8  49103  funcringcsetclem8ALTV  49126  lindslinindsimp2lem5  49283  nn0sumshdig  49444  prelrrx2b  49535  itscnhlc0yqe  49580  iscnrm3lem2  49754  diag1f1lem  50125  spd  50497  setrec1lem4  50509  setrec2fun  50511  aacllem  50662