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  2326  equs5eALT  2371  ax13lem1  2378  nfeqf  2385  hbae  2435  ax12vALT  2473  2ax6elem  2474  sb1  2482  euimmo  2616  necon2ad  2947  necon4ad  2951  r19.37v  3163  spcimgfi1OLD  3493  rr19.28v  3610  moeq3  3658  reuimrmo  3691  sbeqalb  3791  replem  5223  csbexg  5245  ralxfrd  5350  ralxfrd2  5354  ralxfrALT  5357  copsexgwOLD  5444  copsexg  5445  pwssun  5523  somo  5578  ssrel  5739  relssres  5987  dmsnopg  6177  dfco2a  6210  dfpo2  6260  frpoinsg  6307  tz7.7  6349  ordunidif  6373  suctr  6411  trsucss  6413  suc11  6432  imadif  6582  dffv2  6935  fvmptd3f  6963  fvmptnf  6970  foco2  7061  fconst5  7161  fvf1pr  7262  isores3  7290  riotaxfrd  7358  ovmpt4g  7514  ovmpos  7515  ov2gf  7516  ovmpodf  7523  sorpsscmpl  7688  abnexg  7710  onint  7744  limuni3  7803  tfisg  7805  tfis  7806  tfinds  7811  limomss  7822  peano5  7844  fo2ndf  8071  frxp  8076  xpord2pred  8095  xpord2indlem  8097  soseq  8109  suppss2  8150  suppssfv  8152  rntpos  8189  fprlem1  8250  fprresex  8260  wfr3g  8269  onfununi  8281  smofvon2  8296  smo11  8304  smoord  8305  tfrlem11  8327  tz7.44-2  8346  tz7.48lem  8380  tz7.48-1  8382  tz7.49  8384  tz7.49c  8385  omordi  8501  omord  8503  omass  8515  oneo  8516  omeulem1  8517  omopth2  8519  oewordri  8528  oeworde  8529  nnmordi  8567  nnmord  8568  omabs  8587  nnneo  8591  omsmo  8594  naddcllem  8612  qsel  8743  eceqoveq  8769  domunsncan  9015  sbthlem1  9025  2pwuninel  9070  mapen  9079  infensuc  9093  rexdif1en  9095  findcard2  9099  pssnn  9103  ssfi  9107  sucdom2  9137  php  9141  onomeneq  9148  0sdom1dom  9156  sdom1  9160  dif1ennnALT  9187  ac6sfi  9194  frfi  9195  unblem1  9202  unblem2  9203  unbnn2  9207  domunfican  9232  fodomfir  9238  ixpfi2  9260  finsschain  9269  unifi3  9272  marypha1lem  9346  oiexg  9450  brwdom3  9497  inf3lem2  9550  inf3lem3  9551  cantnfval2  9590  cantnflt  9593  cantnflem1  9610  cnfcom  9621  ttrclss  9641  trcl  9649  epfrs  9652  frmin  9673  frinsg  9675  frr3g  9680  frrlem15  9681  r1sdom  9698  cardsdomel  9898  carduni  9905  infpwfien  9984  carduniima  10018  dfac5  10051  dfac12r  10069  dfac12k  10070  kmlem11  10083  djuinf  10111  infxp  10136  cfsuc  10179  cfcoflem  10194  coftr  10195  infpssr  10230  fin23lem30  10264  isf32lem1  10275  isf34lem6  10302  fin1a2lem13  10334  fin1a2s  10336  axcc2lem  10358  domtriomlem  10364  axcclem  10379  ac6num  10401  zorn2lem5  10422  zorn2lem6  10423  axdclem2  10442  alephval2  10495  alephreg  10505  pwcfsdom  10506  axregndlem1  10525  axregnd  10527  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacnd  10535  gchi  10547  fpwwe2lem12  10565  canthp1  10577  gchpwdom  10593  wunfi  10644  tskwe2  10696  inar1  10698  gruen  10735  intgru  10737  indpi  10830  nqereu  10852  ltbtwnnq  10901  prnmadd  10920  genpcd  10929  prlem934  10956  ltexprlem1  10959  ltexprlem2  10960  ltexprlem7  10965  ltaprlem  10967  ltapr  10968  reclem4pr  10973  suplem2pr  10976  mulcmpblnr  10994  recexsrlem  11026  mulgt0sr  11028  supsrlem  11034  axpre-sup  11092  1re  11144  dedekindle  11310  addlsub  11566  recex  11782  nnunb  12433  0mnnnnn0  12469  prime  12610  zeo  12615  fnn0ind  12628  zindd  12630  btwnz  12632  lbzbi  12886  xrub  13264  elfznelfzo  13728  fvf1tp  13748  addmodlteq  13908  facwordi  14251  fiinfnf1o  14312  hashclb  14320  hashdom  14341  hashf1lem2  14418  seqcoll  14426  brfi1indALT  14472  ccatalpha  14556  pfxccatin12lem2a  14689  limsupbnd2  15445  rlimdm  15513  o1of2  15575  rlimno1  15616  isercoll  15630  caurcvg2  15640  caucvgb  15642  serf0  15643  zsum  15680  fsum2dlem  15732  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  zprod  15902  fprod2dlem  15945  fprod2d  15946  odd2np1  16310  ndvdssub  16378  dfgcd2  16515  nprm  16657  maxprmfct  16679  rpexp  16692  pc2dvds  16850  pcfac  16870  unbenlem  16879  4sqlem12  16927  4sqlem17  16932  vdwlem13  16964  prmlem0  17076  mreiincl  17558  sscfn1  17784  initoid  17968  termoid  17969  funcestrcsetclem8  18113  funcsetcestrclem8  18128  pospo  18309  cnvpsb  18545  dirtr  18568  mulgaddcom  19074  mulginvcom  19075  gaass  19272  cntz2ss  19310  elsymgbas  19349  symgfix2  19391  pmtrfrn  19433  psgnran  19490  odmulg  19531  odhash3  19551  sylow2alem1  19592  sylow2alem2  19593  pj1eu  19671  efgs1b  19711  efgsfo  19714  efgredlemc  19720  efgredeu  19727  frgpuptinv  19746  lt6abl  19870  ghmcyg  19871  ablfac1eulem  20049  pgpfac1lem5  20056  ablsimpgfindlem1  20084  gsumle  20120  ringinvnz1ne0  20281  irredmul  20409  rnghmsscmap2  20606  rnghmsscmap  20607  rhmsscmap2  20635  rhmsscmap  20636  acsfn1p  20776  lspextmo  21051  lspsncv0  21144  pzriprnglem12  21472  psgnghm  21560  mplcoe1  22015  mplcoe5  22018  evlseu  22061  mhpsclcl  22113  mdetunilem7  22583  mdetunilem9  22585  chcoeffeq  22851  cnindis  23257  lmss  23263  lmcls  23267  lmcnp  23269  hausnei  23293  cmpsub  23365  tgcmp  23366  fiuncmp  23369  cmpfi  23373  bwth  23375  1stcrest  23418  2ndcdisj  23421  1stccnp  23427  comppfsc  23497  1stckgenlem  23518  txcls  23569  txcn  23591  txlm  23613  tx1stc  23615  xkococn  23625  hmphdis  23761  ptcmpfi  23778  isfild  23823  fgss2  23839  filconn  23848  trfil2  23852  ufileu  23884  filufint  23885  elfm2  23913  flftg  23961  fclssscls  23983  fclscf  23990  ufilcmp  23997  cnpfcf  24006  alexsubb  24011  alexsubALTlem4  24015  alexsubALT  24016  qustgpopn  24085  tsmsxp  24120  isust  24169  xmettri2  24305  blin2  24394  setsmstopn  24443  met2ndc  24488  metcnp3  24505  tngtopn  24615  reconnlem2  24793  xrge0tsms  24800  fsumcn  24837  bndth  24925  iscmet3lem2  25259  iscmet3  25260  ivthlem1  25418  ivthlem2  25419  ivthlem3  25420  ovolfiniun  25468  volfiniun  25514  ioombl1lem4  25528  ismbf3d  25621  mbfi1flimlem  25689  itg2seq  25709  itgfsum  25794  ellimc3  25846  dvmptfsum  25942  c1liplem1  25963  plypf1  26177  plydivex  26263  aannenlem1  26294  ulmval  26345  ulmcau  26360  ulmbdd  26363  ulmcn  26364  ulmdvlem3  26367  sineq0  26488  efopn  26622  cxpeq  26721  logbgcd1irr  26758  rlimcnp  26929  xrlimcnp  26932  lgsdir2lem2  27289  lgsne0  27298  2lgsoddprm  27379  2sqlem6  27386  2sqlem10  27391  2sqreunnltblem  27414  ltsval2  27620  noetasuplem4  27700  conway  27771  madebdayim  27880  addsass  27997  oncutlt  28256  oniso  28263  addonbday  28271  n0ssoldg  28345  bdayn0p1  28361  oldfib  28369  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  z12bdaylem1  28462  z12zsodd  28474  axcontlem2  29034  uhgr0vb  29141  uvtx01vtx  29466  uvtxupgrres  29477  fusgrn0degnn0  29568  finsumvtxdg2size  29619  cusgrm1rusgr  29651  wlkv0  29718  wlklenvclwlk  29722  uspgrn2crct  29876  frrusgrord  30411  numclwwlk1lem2fo  30428  isgrpo  30568  grpoidinvlem3  30577  vcdi  30636  vcdir  30637  vcass  30638  nvs  30734  nvtri  30741  blocnilem  30875  chintcli  31402  hsupss  31412  shlej1  31431  elspansn4  31644  spansncvi  31723  hoaddsub  31887  lnopl  31985  lnfnl  32002  riesz4i  32134  pjnormssi  32239  pj3si  32278  stlei  32311  stcltr2i  32346  dmdmd  32371  dmdbr5  32379  mdslmd1lem2  32397  atssma  32449  atcvatlem  32456  chirredlem1  32461  atcvat4i  32468  mdsymlem2  32475  mdsymlem6  32479  sumdmdlem2  32490  cdjreui  32503  elimifd  32613  disjxpin  32658  xrge0infss  32833  expgt0b  32890  xrge0tsmsd  33134  gsumvsca1  33287  gsumvsca2  33288  lmxrge0  34096  ismeas  34343  eulerpartlemb  34512  bnj849  35067  bnj1110  35124  srcmpltd  35222  axprALT2  35253  trssfir1om  35255  fineqvinfep  35269  trssfir1omregs  35280  swrdrevpfx  35299  cusgredgex2  35305  subgrwlk  35314  cusgr3cyclex  35318  umgr2cycllem  35322  umgr2cycl  35323  connpconn  35417  cvmseu  35458  cvmliftlem15  35480  cvmlift2lem1  35484  cvmlift2lem12  35496  satfv0fun  35553  satffunlem  35583  mclsind  35752  r1peuqusdeg1  35825  dfon2lem3  35965  dfon2lem4  35966  dfon2lem6  35968  dfon2lem8  35970  dfon2lem9  35971  hbntg  35985  cgrdegen  36186  funtransport  36213  ifscgr  36226  cgrxfr  36237  brofs2  36259  brifs2  36260  idinside  36266  btwnconn1lem7  36275  btwnconn1lem11  36279  btwnconn1lem12  36280  btwnconn1lem14  36282  broutsideof2  36304  btwnoutside  36307  outsideoftr  36311  in-ax8  36406  ss-ax8  36407  finminlem  36500  ntruni  36509  neibastop1  36541  ontgval  36613  ordtop  36618  ordcmp  36629  onint1  36631  bj-alrimdh  36889  bj-spimnfe  36918  bj-spimenfa  36919  bj-cbveximd  36926  bj-spvew  36930  bj-cbvexvv  36934  bj-ax12w  36972  axc11n11r  36980  bj-ax12v3  36982  bj-nnfan  37051  bj-nnfand  37052  bj-19.42t  37062  bj-sbft  37075  bj-nnflemea  37086  bj-hbaeb2  37125  bj-spcimdv  37202  bj-spcimdvv  37203  bj-sngltag  37290  bj-xtagex  37296  bj-axseprep  37381  bj-0int  37413  bj-ismooredr  37421  bj-inftyexpiinj  37523  nlpfvineqsn  37725  wl-ax13lem1  37810  wl-speqv  37847  wl-sbcom2d  37886  tan2h  37933  ptrest  37940  poimirlem20  37961  poimirlem22  37963  poimirlem26  37967  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  heicant  37976  voliunnfl  37985  volsupnfl  37986  itg2addnclem2  37993  itg2addnc  37995  itg2gt0cn  37996  ftc2nc  38023  filbcmb  38061  sdclem2  38063  seqpo  38068  nninfnub  38072  neificl  38074  prdstotbnd  38115  cnpwstotbnd  38118  heibor1lem  38130  heibor  38142  bfplem2  38144  opidonOLD  38173  exidu1  38177  grpokerinj  38214  rngoideu  38224  rngodi  38225  rngodir  38226  rngmgmbs4  38252  divrngidl  38349  prnc  38388  rsp3eq  38688  eqvrelqsel  39021  erimeq2  39084  prter2  39327  ax4fromc4  39340  hbae-o  39349  dvelimf-o  39375  ax12indn  39389  ax12inda2  39393  ax12a2-o  39396  l1cvpat  39500  atcvrj0  39874  pmaple  40207  paddasslem5  40270  pclfinN  40346  osumcllem11N  40412  pexmidlem8N  40423  dvheveccl  41558  dihord6apre  41702  lpolconN  41933  lcmineqlem1  42468  oexpreposd  42754  sn-it0e0  42848  cnreeu  42935  eu6w  43109  isnacs3  43142  pellexlem5  43261  pellex  43263  jm2.18  43416  jm2.15nn0  43431  jm2.16nn0  43432  dford3lem2  43455  ttac  43464  onexomgt  43669  onexoegt  43672  omabs2  43760  omcl3g  43762  tfsconcat0b  43774  naddgeoa  43822  safesnsupfiss  43842  rp-isfinite5  43944  cnvssb  44013  clcnvlem  44050  iunrelexpuztr  44146  rfovcnvf1od  44431  ntrrn  44549  nzss  44744  pm11.71  44824  axc11next  44833  hbntal  44980  eel2122old  45144  relwf  45394  modelaxreplem1  45405  ssclaxsep  45409  wfac8prim  45429  fsetsnf1  47500  2reu8i  47561  afvelima  47615  rlimdmafv  47625  rlimdmafv2  47706  elsprel  47935  sfprmdvdsmersenne  48066  perfectALTVlem2  48198  fpprwppr  48215  uhgrimedgi  48366  isuspgrim0lem  48369  uhgrimisgrgric  48407  gpgcubic  48555  gpg5nbgr3star  48557  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  copisnmnd  48645  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  lindslinindsimp2lem5  48938  nn0sumshdig  49099  prelrrx2b  49190  itscnhlc0yqe  49235  iscnrm3lem2  49410  diag1f1lem  49781  spd  50153  setrec1lem4  50165  setrec2fun  50167  aacllem  50276