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  136  con3d  155  nsyli  160  syl5bi  245  syl5bir  246  syl5ib  247  adantld  494  adantrd  495  impel  509  mpan9  510  pm4.72  950  pm2.36  970  pm4.79  1004  ecased  1035  ecase3adOLD  1037  alrimdh  1871  stdpc5v  1946  19.37imv  1956  ax12w  2133  ax13dgen2  2138  ax12v  2176  spsd  2184  nf5r  2191  nf5rOLD  2192  axc4  2320  equs5eALT  2366  ax13lem1  2373  nfeqf  2380  hbae  2430  ax12vALT  2468  2ax6elem  2469  sb1  2478  euimmo  2617  necon2ad  2955  necon4ad  2959  r19.37v  3258  spcimgft  3502  rr19.28v  3577  moeq3  3625  reuimrmo  3658  sbeqalb  3763  csbexg  5203  ralxfrd  5301  ralxfrd2  5305  ralxfrALT  5308  copsexgw  5373  copsexg  5374  pwssun  5451  somo  5505  ssrel  5654  relssres  5892  dmsnopg  6076  dfco2a  6110  frpoinsg  6197  wfisg  6205  tz7.7  6239  ordunidif  6261  suctr  6296  trsucss  6298  suc11  6316  imadif  6464  dffv2  6806  fvmptd3f  6833  fvmptnf  6840  foco2  6926  fconst5  7021  isores3  7144  riotaxfrd  7205  ovmpt4g  7356  ovmpos  7357  ov2gf  7358  ovmpodf  7365  sorpsscmpl  7522  abnexg  7541  onint  7574  limuni3  7631  tfis  7633  tfinds  7638  limomss  7649  peano5  7671  peano5OLD  7672  fo2ndf  7890  frxp  7893  suppss2  7942  suppssfv  7944  rntpos  7981  fprlem1  8041  wfr3g  8053  wfrlem5  8059  wfrlem17  8071  onfununi  8078  smofvon2  8093  smo11  8101  smoord  8102  tfrlem11  8124  tz7.44-2  8143  tz7.48lem  8177  tz7.48-1  8179  tz7.49  8181  tz7.49c  8182  omordi  8294  omord  8296  omass  8308  oneo  8309  omeulem1  8310  omopth2  8312  oewordri  8320  oeworde  8321  nnmordi  8359  nnmord  8360  omabs  8376  nnneo  8380  omsmo  8383  qsel  8478  eceqoveq  8504  domunsncan  8745  sucdom2  8755  sbthlem1  8756  2pwuninel  8801  mapen  8810  infensuc  8824  findcard2  8842  pssnn  8846  ssfi  8851  pssnnOLD  8895  dif1enALT  8907  findcard2OLD  8913  ac6sfi  8915  frfi  8916  unblem1  8923  unblem2  8924  unbnn2  8928  nnsdomg  8930  xpfi  8942  domunfican  8944  fiint  8948  ixpfi2  8974  finsschain  8983  marypha1lem  9049  oiexg  9151  brwdom3  9198  inf3lem2  9244  inf3lem3  9245  cantnfval2  9284  cantnflt  9287  cantnflem1  9304  cnfcom  9315  dftrpred3g  9339  trpredrec  9342  trcl  9344  epfrs  9347  frinsg  9367  frr3g  9372  frrlem15  9373  r1sdom  9390  cardsdomel  9590  carduni  9597  pr2ne  9619  infpwfien  9676  carduniima  9710  dfac5  9742  dfac12r  9760  dfac12k  9761  kmlem11  9774  djuinf  9802  infxp  9829  cfsuc  9871  cfcoflem  9886  coftr  9887  infpssr  9922  fin23lem30  9956  isf32lem1  9967  isf34lem6  9994  fin1a2lem13  10026  fin1a2s  10028  axcc2lem  10050  domtriomlem  10056  axcclem  10071  ac6num  10093  zorn2lem5  10114  zorn2lem6  10115  axdclem2  10134  alephval2  10186  alephreg  10196  pwcfsdom  10197  axregndlem1  10216  axregnd  10218  axacndlem1  10221  axacndlem2  10222  axacndlem3  10223  axacndlem4  10224  axacnd  10226  gchi  10238  fpwwe2lem12  10256  canthp1  10268  gchpwdom  10284  wunfi  10335  tskwe2  10387  inar1  10389  gruen  10426  intgru  10428  indpi  10521  nqereu  10543  ltbtwnnq  10592  prnmadd  10611  genpcd  10620  prlem934  10647  ltexprlem1  10650  ltexprlem2  10651  ltexprlem7  10656  ltaprlem  10658  ltapr  10659  reclem4pr  10664  suplem2pr  10667  mulcmpblnr  10685  recexsrlem  10717  mulgt0sr  10719  supsrlem  10725  axpre-sup  10783  1re  10833  dedekindle  10996  addlsub  11248  recex  11464  nnunb  12086  0mnnnnn0  12122  prime  12258  zeo  12263  fnn0ind  12276  zindd  12278  btwnz  12279  lbzbi  12532  xrub  12902  elfznelfzo  13347  addmodlteq  13519  facwordi  13855  fiinfnf1o  13916  hashclb  13925  hashdom  13946  hashf1lem2  14022  seqcoll  14030  brfi1indALT  14066  ccatalpha  14150  pfxccatin12lem2a  14292  limsupbnd2  15044  rlimdm  15112  o1of2  15174  rlimno1  15217  isercoll  15231  caurcvg2  15241  caucvgb  15243  serf0  15244  zsum  15282  fsum2dlem  15334  fsum2d  15335  fsumabs  15365  fsumrlim  15375  fsumo1  15376  fsumiun  15385  zprod  15499  fprod2dlem  15542  fprod2d  15543  odd2np1  15902  ndvdssub  15970  dfgcd2  16106  nprm  16245  maxprmfct  16266  rpexp  16279  pc2dvds  16432  pcfac  16452  unbenlem  16461  4sqlem12  16509  4sqlem17  16514  vdwlem13  16546  prmlem0  16659  mreiincl  17099  sscfn1  17322  initoid  17507  termoid  17508  funcestrcsetclem8  17654  funcsetcestrclem8  17669  pospo  17851  cnvpsb  18085  dirtr  18108  mulgaddcom  18515  mulginvcom  18516  gaass  18691  cntz2ss  18727  elsymgbas  18766  symgfix2  18808  pmtrfrn  18850  psgnran  18907  odmulg  18947  odhash3  18965  sylow2alem1  19006  sylow2alem2  19007  pj1eu  19086  efgs1b  19126  efgsfo  19129  efgredlemc  19135  efgredeu  19142  frgpuptinv  19161  lt6abl  19280  ghmcyg  19281  ablfac1eulem  19459  pgpfac1lem5  19466  ablsimpgfindlem1  19494  ringinvnz1ne0  19610  irredmul  19727  acsfn1p  19843  lspextmo  20093  lspsncv0  20183  psgnghm  20542  mplcoe1  20994  mplcoe5  20997  evlseu  21043  mhpsclcl  21087  mdetunilem7  21515  mdetunilem9  21517  chcoeffeq  21783  cnindis  22189  lmss  22195  lmcls  22199  lmcnp  22201  hausnei  22225  cmpsub  22297  tgcmp  22298  fiuncmp  22301  cmpfi  22305  bwth  22307  1stcrest  22350  2ndcdisj  22353  1stccnp  22359  comppfsc  22429  1stckgenlem  22450  txcls  22501  txcn  22523  txlm  22545  tx1stc  22547  xkococn  22557  hmphdis  22693  ptcmpfi  22710  isfild  22755  fgss2  22771  filconn  22780  trfil2  22784  ufileu  22816  filufint  22817  elfm2  22845  flftg  22893  fclssscls  22915  fclscf  22922  ufilcmp  22929  cnpfcf  22938  alexsubb  22943  alexsubALTlem4  22947  alexsubALT  22948  qustgpopn  23017  tsmsxp  23052  isust  23101  xmettri2  23238  blin2  23327  setsmstopn  23376  met2ndc  23421  metcnp3  23438  tngtopn  23548  reconnlem2  23724  xrge0tsms  23731  fsumcn  23767  bndth  23855  iscmet3lem2  24189  iscmet3  24190  ivthlem1  24348  ivthlem2  24349  ivthlem3  24350  ovolfiniun  24398  volfiniun  24444  ioombl1lem4  24458  ismbf3d  24551  mbfi1flimlem  24620  itg2seq  24640  itgfsum  24724  ellimc3  24776  dvmptfsum  24872  c1liplem1  24893  plypf1  25106  plydivex  25190  aannenlem1  25221  ulmval  25272  ulmcau  25287  ulmbdd  25290  ulmcn  25291  ulmdvlem3  25294  sineq0  25413  efopn  25546  cxpeq  25643  logbgcd1irr  25677  rlimcnp  25848  xrlimcnp  25851  lgsdir2lem2  26207  lgsne0  26216  2lgsoddprm  26297  2sqlem6  26304  2sqlem10  26309  2sqreunnltblem  26332  axcontlem2  27056  uhgr0vb  27163  uvtx01vtx  27485  uvtxupgrres  27496  fusgrn0degnn0  27587  finsumvtxdg2size  27638  cusgrm1rusgr  27670  wlkv0  27738  wlklenvclwlk  27742  uspgrn2crct  27892  frrusgrord  28424  numclwwlk1lem2fo  28441  isgrpo  28578  grpoidinvlem3  28587  vcdi  28646  vcdir  28647  vcass  28648  nvs  28744  nvtri  28751  blocnilem  28885  chintcli  29412  hsupss  29422  shlej1  29441  elspansn4  29654  spansncvi  29733  hoaddsub  29897  lnopl  29995  lnfnl  30012  riesz4i  30144  pjnormssi  30249  pj3si  30288  stlei  30321  stcltr2i  30356  dmdmd  30381  dmdbr5  30389  mdslmd1lem2  30407  atssma  30459  atcvatlem  30466  chirredlem1  30471  atcvat4i  30478  mdsymlem2  30485  mdsymlem6  30489  sumdmdlem2  30500  cdjreui  30513  elimifd  30605  disjxpin  30646  unifi3  30767  xrge0infss  30803  xrge0tsmsd  31036  gsumle  31069  gsumvsca1  31198  gsumvsca2  31199  lmxrge0  31616  ismeas  31879  eulerpartlemb  32047  bnj849  32618  bnj1110  32675  srcmpltd  32767  swrdrevpfx  32791  cusgredgex2  32797  subgrwlk  32807  cusgr3cyclex  32811  umgr2cycllem  32815  umgr2cycl  32816  connpconn  32910  cvmseu  32951  cvmliftlem15  32973  cvmlift2lem1  32977  cvmlift2lem12  32989  satfv0fun  33046  satffunlem  33076  mclsind  33245  dfpo2  33441  dfon2lem3  33480  dfon2lem4  33481  dfon2lem6  33483  dfon2lem8  33485  dfon2lem9  33486  hbntg  33500  tfisg  33505  ttrclss  33519  xpord2pred  33529  xpord2ind  33531  xpord3ind  33537  soseq  33540  naddcllem  33568  sltval2  33596  noetasuplem4  33676  conway  33730  madebdayim  33807  cgrdegen  34043  funtransport  34070  ifscgr  34083  cgrxfr  34094  brofs2  34116  brifs2  34117  idinside  34123  btwnconn1lem7  34132  btwnconn1lem11  34136  btwnconn1lem12  34137  btwnconn1lem14  34139  broutsideof2  34161  btwnoutside  34164  outsideoftr  34168  finminlem  34244  ntruni  34253  neibastop1  34285  ontgval  34357  ordtop  34362  ordcmp  34373  onint1  34375  bj-ax12w  34595  axc11n11r  34602  bj-ax12v3  34604  bj-nnfan  34667  bj-nnfand  34668  bj-nnflemea  34684  bj-19.42t  34692  bj-sbft  34694  bj-hbaeb2  34738  bj-spcimdv  34817  bj-spcimdvv  34818  bj-sngltag  34910  bj-xtagex  34916  bj-0int  35007  bj-ismooredr  35015  bj-inftyexpiinj  35115  nlpfvineqsn  35317  wl-ax13lem1  35402  wl-speqv  35418  wl-sbcom2d  35453  wl-ax11-lem3  35475  wl-ax11-lem8  35480  tan2h  35506  ptrest  35513  poimirlem20  35534  poimirlem22  35536  poimirlem26  35540  poimirlem30  35544  poimirlem31  35545  poimirlem32  35546  heicant  35549  voliunnfl  35558  volsupnfl  35559  itg2addnclem2  35566  itg2addnc  35568  itg2gt0cn  35569  ftc2nc  35596  filbcmb  35635  sdclem2  35637  seqpo  35642  nninfnub  35646  neificl  35648  prdstotbnd  35689  cnpwstotbnd  35692  heibor1lem  35704  heibor  35716  bfplem2  35718  opidonOLD  35747  exidu1  35751  grpokerinj  35788  rngoideu  35798  rngodi  35799  rngodir  35800  rngmgmbs4  35826  divrngidl  35923  prnc  35962  eqvrelqsel  36466  erim2  36526  prter2  36632  ax4fromc4  36645  hbae-o  36654  dvelimf-o  36680  ax12indn  36694  ax12inda2  36698  ax12a2-o  36701  l1cvpat  36805  atcvrj0  37179  pmaple  37512  paddasslem5  37575  pclfinN  37651  osumcllem11N  37717  pexmidlem8N  37728  dvheveccl  38863  dihord6apre  39007  lpolconN  39238  lcmineqlem1  39771  oexpreposd  40028  sn-it0e0  40105  cnreeu  40146  isnacs3  40235  pellexlem5  40358  pellex  40360  jm2.18  40513  jm2.15nn0  40528  jm2.16nn0  40529  dford3lem2  40552  ttac  40561  rp-isfinite5  40809  cnvssb  40870  clcnvlem  40907  iunrelexpuztr  41004  rfovcnvf1od  41289  ntrrn  41409  nzss  41608  pm11.71  41688  axc11next  41697  hbntal  41846  eel2122old  42011  fsetsnf1  44218  2reu8i  44277  afvelima  44331  rlimdmafv  44341  rlimdmafv2  44422  elsprel  44600  sfprmdvdsmersenne  44728  perfectALTVlem2  44847  fpprwppr  44864  copisnmnd  45036  rnghmsscmap2  45204  rnghmsscmap  45205  rhmsscmap2  45250  rhmsscmap  45251  funcringcsetcALTV2lem8  45274  funcringcsetclem8ALTV  45297  lindslinindsimp2lem5  45476  nn0sumshdig  45642  prelrrx2b  45733  itscnhlc0yqe  45778  iscnrm3lem2  45901  spd  46055  setrec1lem4  46067  setrec2fun  46069  aacllem  46176