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  243  biimtrrid  244  imbitrid  245  adantld  491  adantrd  492  impel  510  mpan9  511  pm4.72  957  pm2.36  977  pm4.79  1011  ecased  1041  alrimdh  1870  stdpc5v  1945  19.37imv  1954  ax12w  2144  ax13dgen2  2149  ax12v  2190  spsd  2199  nf5r  2206  axc4  2330  equs5eALT  2375  ax13lem1  2382  nfeqf  2389  hbae  2439  ax12vALT  2477  2ax6elem  2478  sb1  2486  euimmo  2620  necon2ad  2950  necon4ad  2954  r19.37v  3166  spcimgfi1OLD  3496  rr19.28v  3613  moeq3  3660  reuimrmo  3693  sbeqalb  3792  replem  5217  csbexg  5239  ralxfrd  5344  ralxfrd2  5348  ralxfrALT  5351  copsexgwOLD  5438  copsexg  5439  pwssun  5517  somo  5572  ssrel  5733  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  6958  fvmptnf  6965  foco2  7057  fconst5  7157  fvf1pr  7258  isores3  7286  riotaxfrd  7354  ovmpt4g  7510  ovmpos  7511  ov2gf  7512  ovmpodf  7519  sorpsscmpl  7684  abnexg  7706  onint  7740  limuni3  7799  tfisg  7801  tfis  7802  tfinds  7807  limomss  7818  peano5  7840  fo2ndf  8067  frxp  8073  xpord2pred  8092  xpord2indlem  8094  soseq  8106  suppss2  8147  suppssfv  8149  rntpos  8186  fprlem1  8247  fprresex  8257  wfr3g  8266  onfununi  8278  smofvon2  8293  smo11  8301  smoord  8302  tfrlem11  8324  tz7.44-2  8343  tz7.48lem  8377  tz7.48-1  8379  tz7.49  8381  tz7.49c  8382  omordi  8498  omord  8500  omass  8512  oneo  8513  omeulem1  8514  omopth2  8516  oewordri  8525  oeworde  8526  nnmordi  8564  nnmord  8565  omabs  8584  nnneo  8588  omsmo  8591  naddcllem  8609  qsel  8740  eceqoveq  8766  domunsncan  9012  sbthlem1  9022  2pwuninel  9067  mapen  9076  infensuc  9090  rexdif1en  9092  findcard2  9096  pssnn  9100  ssfi  9104  sucdom2  9134  php  9138  onomeneq  9145  0sdom1dom  9153  sdom1  9157  dif1ennnALT  9184  ac6sfi  9191  frfi  9192  unblem1  9199  unblem2  9200  unbnn2  9204  domunfican  9229  fodomfir  9235  ixpfi2  9257  finsschain  9266  unifi3  9269  marypha1lem  9343  oiexg  9447  brwdom3  9494  inf3lem2  9548  inf3lem3  9549  cantnfval2  9588  cantnflt  9591  cantnflem1  9608  cnfcom  9619  ttrclss  9639  trcl  9647  epfrs  9650  frmin  9671  frinsg  9673  frr3g  9678  frrlem15  9679  r1sdom  9696  cardsdomel  9896  carduni  9903  infpwfien  9982  carduniima  10016  dfac5  10049  dfac12r  10067  dfac12k  10068  kmlem11  10081  djuinf  10109  infxp  10134  cfsuc  10177  cfcoflem  10192  coftr  10193  infpssr  10228  fin23lem30  10262  isf32lem1  10273  isf34lem6  10300  fin1a2lem13  10332  fin1a2s  10334  axcc2lem  10356  domtriomlem  10362  axcclem  10377  ac6num  10399  zorn2lem5  10420  zorn2lem6  10421  axdclem2  10440  alephval2  10493  alephreg  10503  pwcfsdom  10504  axregndlem1  10523  axregnd  10525  axacndlem1  10528  axacndlem2  10529  axacndlem3  10530  axacndlem4  10531  axacnd  10533  gchi  10545  fpwwe2lem12  10563  canthp1  10575  gchpwdom  10591  wunfi  10642  tskwe2  10694  inar1  10696  gruen  10733  intgru  10735  indpi  10828  nqereu  10850  ltbtwnnq  10899  prnmadd  10918  genpcd  10927  prlem934  10954  ltexprlem1  10957  ltexprlem2  10958  ltexprlem7  10963  ltaprlem  10965  ltapr  10966  reclem4pr  10971  suplem2pr  10974  mulcmpblnr  10992  recexsrlem  11024  mulgt0sr  11026  supsrlem  11032  axpre-sup  11090  1re  11142  dedekindle  11308  addlsub  11564  recex  11780  nnunb  12431  0mnnnnn0  12467  prime  12608  zeo  12613  fnn0ind  12626  zindd  12628  btwnz  12630  lbzbi  12884  xrub  13262  elfznelfzo  13726  fvf1tp  13746  addmodlteq  13906  facwordi  14249  fiinfnf1o  14310  hashclb  14318  hashdom  14339  hashf1lem2  14416  seqcoll  14424  brfi1indALT  14470  ccatalpha  14554  pfxccatin12lem2a  14687  limsupbnd2  15443  rlimdm  15511  o1of2  15573  rlimno1  15614  isercoll  15628  caurcvg2  15638  caucvgb  15640  serf0  15641  zsum  15678  fsum2dlem  15730  fsum2d  15731  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  zprod  15900  fprod2dlem  15943  fprod2d  15944  odd2np1  16308  ndvdssub  16376  dfgcd2  16513  nprm  16655  maxprmfct  16677  rpexp  16690  pc2dvds  16848  pcfac  16868  unbenlem  16877  4sqlem12  16925  4sqlem17  16930  vdwlem13  16962  prmlem0  17074  mreiincl  17556  sscfn1  17782  initoid  17966  termoid  17967  funcestrcsetclem8  18111  funcsetcestrclem8  18126  pospo  18307  cnvpsb  18543  dirtr  18566  mulgaddcom  19072  mulginvcom  19073  gaass  19270  cntz2ss  19308  elsymgbas  19347  symgfix2  19389  pmtrfrn  19431  psgnran  19488  odmulg  19529  odhash3  19549  sylow2alem1  19590  sylow2alem2  19591  pj1eu  19669  efgs1b  19709  efgsfo  19712  efgredlemc  19718  efgredeu  19725  frgpuptinv  19744  lt6abl  19868  ghmcyg  19869  ablfac1eulem  20047  pgpfac1lem5  20054  ablsimpgfindlem1  20082  gsumle  20118  ringinvnz1ne0  20279  irredmul  20407  rnghmsscmap2  20608  rnghmsscmap  20609  rhmsscmap2  20637  rhmsscmap  20638  acsfn1p  20778  lspextmo  21053  lspsncv0  21146  pzriprnglem12  21474  psgnghm  21562  mplcoe1  22020  mplcoe5  22023  evlseu  22066  mhpsclcl  22142  mdetunilem7  22608  mdetunilem9  22610  chcoeffeq  22876  cnindis  23282  lmss  23288  lmcls  23292  lmcnp  23294  hausnei  23318  cmpsub  23390  tgcmp  23391  fiuncmp  23394  cmpfi  23398  bwth  23400  1stcrest  23443  2ndcdisj  23446  1stccnp  23452  comppfsc  23522  1stckgenlem  23543  txcls  23594  txcn  23616  txlm  23638  tx1stc  23640  xkococn  23650  hmphdis  23786  ptcmpfi  23803  isfild  23848  fgss2  23864  filconn  23873  trfil2  23877  ufileu  23909  filufint  23910  elfm2  23938  flftg  23986  fclssscls  24008  fclscf  24015  ufilcmp  24022  cnpfcf  24031  alexsubb  24036  alexsubALTlem4  24040  alexsubALT  24041  qustgpopn  24110  tsmsxp  24145  isust  24194  xmettri2  24330  blin2  24419  setsmstopn  24468  met2ndc  24513  metcnp3  24530  tngtopn  24640  reconnlem2  24818  xrge0tsms  24825  fsumcn  24862  bndth  24950  iscmet3lem2  25284  iscmet3  25285  ivthlem1  25443  ivthlem2  25444  ivthlem3  25445  ovolfiniun  25493  volfiniun  25539  ioombl1lem4  25553  ismbf3d  25646  mbfi1flimlem  25714  itg2seq  25734  itgfsum  25819  ellimc3  25871  dvmptfsum  25967  c1liplem1  25988  plypf1  26202  plydivex  26288  aannenlem1  26319  ulmval  26370  ulmcau  26385  ulmbdd  26388  ulmcn  26389  ulmdvlem3  26392  sineq0  26513  efopn  26647  cxpeq  26746  logbgcd1irr  26783  rlimcnp  26954  xrlimcnp  26957  lgsdir2lem2  27314  lgsne0  27323  2lgsoddprm  27404  2sqlem6  27411  2sqlem10  27416  2sqreunnltblem  27439  ltsval2  27645  noetasuplem4  27725  conway  27796  madebdayim  27905  addsass  28022  oncutlt  28281  oniso  28288  addonbday  28296  n0ssoldg  28370  bdayn0p1  28386  oldfib  28394  bdaypw2n0bndlem  28480  bdayfinbndlem1  28484  z12bdaylem1  28487  z12zsodd  28499  axcontlem2  29059  uhgr0vb  29166  uvtx01vtx  29491  uvtxupgrres  29502  fusgrn0degnn0  29593  finsumvtxdg2size  29644  cusgrm1rusgr  29676  wlkv0  29743  wlklenvclwlk  29747  uspgrn2crct  29901  frrusgrord  30436  numclwwlk1lem2fo  30453  isgrpo  30593  grpoidinvlem3  30602  vcdi  30661  vcdir  30662  vcass  30663  nvs  30759  nvtri  30766  blocnilem  30900  chintcli  31427  hsupss  31437  shlej1  31456  elspansn4  31669  spansncvi  31748  hoaddsub  31912  lnopl  32010  lnfnl  32027  riesz4i  32159  pjnormssi  32264  pj3si  32303  stlei  32336  stcltr2i  32371  dmdmd  32396  dmdbr5  32404  mdslmd1lem2  32422  atssma  32474  atcvatlem  32481  chirredlem1  32486  atcvat4i  32493  mdsymlem2  32500  mdsymlem6  32504  sumdmdlem2  32515  cdjreui  32528  elimifd  32638  disjxpin  32684  xrge0infss  32859  expgt0b  32916  xrge0tsmsd  33161  gsumvsca1  33314  gsumvsca2  33315  lmxrge0  34143  ismeas  34390  eulerpartlemb  34559  bnj849  35114  bnj1110  35171  srcmpltd  35269  axprALT2  35297  trssfir1om  35299  fineqvinfep  35313  trssfir1omregs  35324  swrdrevpfx  35352  cusgredgex2  35358  subgrwlk  35367  cusgr3cyclex  35371  umgr2cycllem  35375  umgr2cycl  35376  connpconn  35470  cvmseu  35511  cvmliftlem15  35533  cvmlift2lem1  35537  cvmlift2lem12  35549  satfv0fun  35606  satffunlem  35636  mclsind  35805  r1peuqusdeg1  35878  dfon2lem3  36018  dfon2lem4  36019  dfon2lem6  36021  dfon2lem8  36023  dfon2lem9  36024  hbntg  36038  cgrdegen  36239  funtransport  36266  ifscgr  36279  cgrxfr  36290  brofs2  36312  brifs2  36313  idinside  36319  btwnconn1lem7  36328  btwnconn1lem11  36332  btwnconn1lem12  36333  btwnconn1lem14  36335  broutsideof2  36357  btwnoutside  36360  outsideoftr  36364  in-ax8  36459  ss-ax8  36460  finminlem  36553  ntruni  36562  neibastop1  36594  ontgval  36666  ordtop  36671  ordcmp  36682  onint1  36684  bj-alrimdh  36942  bj-spimnfe  36971  bj-spimenfa  36972  bj-cbveximd  36979  bj-spvew  36983  bj-cbvexvv  36987  bj-ax12w  37025  axc11n11r  37033  bj-ax12v3  37035  bj-nnfan  37104  bj-nnfand  37105  bj-19.42t  37115  bj-sbft  37128  bj-nnflemea  37139  bj-hbaeb2  37178  bj-spcimdv  37255  bj-spcimdvv  37256  bj-sngltag  37343  bj-xtagex  37349  bj-axseprep  37434  bj-0int  37466  bj-ismooredr  37474  bj-inftyexpiinj  37576  nlpfvineqsn  37778  wl-ax13lem1  37863  wl-speqv  37900  wl-sbcom2d  37939  tan2h  37986  ptrest  37993  poimirlem20  38014  poimirlem22  38016  poimirlem26  38020  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  heicant  38029  voliunnfl  38038  volsupnfl  38039  itg2addnclem2  38046  itg2addnc  38048  itg2gt0cn  38049  ftc2nc  38076  filbcmb  38114  sdclem2  38116  seqpo  38121  nninfnub  38125  neificl  38127  prdstotbnd  38168  cnpwstotbnd  38171  heibor1lem  38183  heibor  38195  bfplem2  38197  opidonOLD  38226  exidu1  38230  grpokerinj  38267  rngoideu  38277  rngodi  38278  rngodir  38279  rngmgmbs4  38305  divrngidl  38402  prnc  38441  rsp3eq  38741  eqvrelqsel  39074  erimeq2  39137  prter2  39380  ax4fromc4  39393  hbae-o  39402  dvelimf-o  39428  ax12indn  39442  ax12inda2  39446  ax12a2-o  39449  l1cvpat  39553  atcvrj0  39927  pmaple  40260  paddasslem5  40323  pclfinN  40399  osumcllem11N  40465  pexmidlem8N  40476  dvheveccl  41611  dihord6apre  41755  lpolconN  41986  lcmineqlem1  42521  oexpreposd  42806  sn-it0e0  42900  cnreeu  42987  eu6w  43133  isnacs3  43166  pellexlem5  43285  pellex  43287  jm2.18  43440  jm2.15nn0  43455  jm2.16nn0  43456  dford3lem2  43479  ttac  43488  onexomgt  43693  onexoegt  43696  omabs2  43784  omcl3g  43786  tfsconcat0b  43798  naddgeoa  43846  safesnsupfiss  43866  rp-isfinite5  43968  cnvssb  44037  clcnvlem  44074  iunrelexpuztr  44170  rfovcnvf1od  44455  ntrrn  44573  nzss  44768  pm11.71  44848  axc11next  44857  hbntal  45004  eel2122old  45168  relwf  45418  modelaxreplem1  45429  ssclaxsep  45433  wfac8prim  45453  fsetsnf1  47522  2reu8i  47583  afvelima  47637  rlimdmafv  47647  rlimdmafv2  47728  elsprel  47957  sfprmdvdsmersenne  48088  perfectALTVlem2  48220  fpprwppr  48237  uhgrimedgi  48388  isuspgrim0lem  48391  uhgrimisgrgric  48429  gpgcubic  48577  gpg5nbgr3star  48579  pgnioedg1  48606  pgnioedg2  48607  pgnioedg3  48608  pgnioedg4  48609  pgnioedg5  48610  copisnmnd  48667  funcringcsetcALTV2lem8  48795  funcringcsetclem8ALTV  48818  lindslinindsimp2lem5  48960  nn0sumshdig  49121  prelrrx2b  49212  itscnhlc0yqe  49257  iscnrm3lem2  49432  diag1f1lem  49803  spd  50175  setrec1lem4  50187  setrec2fun  50189  aacllem  50298