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  1863  stdpc5v  1938  19.37imv  1947  ax12w  2133  ax13dgen2  2138  ax12v  2178  spsd  2187  nf5r  2194  axc4  2321  equs5eALT  2370  ax13lem1  2379  nfeqf  2386  hbae  2436  ax12vALT  2474  2ax6elem  2475  sb1  2483  euimmo  2616  necon2ad  2955  necon4ad  2959  r19.37v  3182  spcimgfi1OLD  3548  rr19.28v  3668  moeq3  3718  reuimrmo  3751  sbeqalb  3853  csbexg  5310  ralxfrd  5408  ralxfrd2  5412  ralxfrALT  5415  copsexgw  5495  copsexg  5496  pwssun  5575  somo  5631  ssrel  5792  ssrelOLD  5793  relssres  6040  dmsnopg  6233  dfco2a  6266  dfpo2  6316  frpoinsg  6364  wfisgOLD  6375  tz7.7  6410  ordunidif  6433  suctr  6470  trsucss  6472  suc11  6491  imadif  6650  dffv2  7004  fvmptd3f  7031  fvmptnf  7038  foco2  7129  fconst5  7226  fvf1pr  7327  isores3  7355  riotaxfrd  7422  ovmpt4g  7580  ovmpos  7581  ov2gf  7582  ovmpodf  7589  sorpsscmpl  7754  abnexg  7776  onint  7810  limuni3  7873  tfisg  7875  tfis  7876  tfinds  7881  limomss  7892  peano5  7915  fo2ndf  8146  frxp  8151  xpord2pred  8170  xpord2indlem  8172  soseq  8184  suppss2  8225  suppssfv  8227  rntpos  8264  fprlem1  8325  fprresex  8335  wfr3g  8347  wfrlem5OLD  8353  wfrlem17OLD  8365  onfununi  8381  smofvon2  8396  smo11  8404  smoord  8405  tfrlem11  8428  tz7.44-2  8447  tz7.48lem  8481  tz7.48-1  8483  tz7.49  8485  tz7.49c  8486  omordi  8604  omord  8606  omass  8618  oneo  8619  omeulem1  8620  omopth2  8622  oewordri  8630  oeworde  8631  nnmordi  8669  nnmord  8670  omabs  8689  nnneo  8693  omsmo  8696  naddcllem  8714  qsel  8836  eceqoveq  8862  domunsncan  9112  sucdom2OLD  9122  sbthlem1  9123  2pwuninel  9172  mapen  9181  infensuc  9195  rexdif1en  9198  findcard2  9204  pssnn  9208  ssfi  9213  sucdom2  9243  php  9247  onomeneq  9265  0sdom1dom  9274  sdom1  9278  dif1ennnALT  9311  ac6sfi  9320  frfi  9321  unblem1  9328  unblem2  9329  unbnn2  9333  nnsdomgOLD  9336  xpfiOLD  9359  domunfican  9361  fiintOLD  9367  fodomfir  9368  ixpfi2  9390  finsschain  9399  marypha1lem  9473  oiexg  9575  brwdom3  9622  inf3lem2  9669  inf3lem3  9670  cantnfval2  9709  cantnflt  9712  cantnflem1  9729  cnfcom  9740  ttrclss  9760  trcl  9768  epfrs  9771  frmin  9789  frinsg  9791  frr3g  9796  frrlem15  9797  r1sdom  9814  cardsdomel  10014  carduni  10021  pr2neOLD  10045  infpwfien  10102  carduniima  10136  dfac5  10169  dfac12r  10187  dfac12k  10188  kmlem11  10201  djuinf  10229  infxp  10254  cfsuc  10297  cfcoflem  10312  coftr  10313  infpssr  10348  fin23lem30  10382  isf32lem1  10393  isf34lem6  10420  fin1a2lem13  10452  fin1a2s  10454  axcc2lem  10476  domtriomlem  10482  axcclem  10497  ac6num  10519  zorn2lem5  10540  zorn2lem6  10541  axdclem2  10560  alephval2  10612  alephreg  10622  pwcfsdom  10623  axregndlem1  10642  axregnd  10644  axacndlem1  10647  axacndlem2  10648  axacndlem3  10649  axacndlem4  10650  axacnd  10652  gchi  10664  fpwwe2lem12  10682  canthp1  10694  gchpwdom  10710  wunfi  10761  tskwe2  10813  inar1  10815  gruen  10852  intgru  10854  indpi  10947  nqereu  10969  ltbtwnnq  11018  prnmadd  11037  genpcd  11046  prlem934  11073  ltexprlem1  11076  ltexprlem2  11077  ltexprlem7  11082  ltaprlem  11084  ltapr  11085  reclem4pr  11090  suplem2pr  11093  mulcmpblnr  11111  recexsrlem  11143  mulgt0sr  11145  supsrlem  11151  axpre-sup  11209  1re  11261  dedekindle  11425  addlsub  11679  recex  11895  nnunb  12522  0mnnnnn0  12558  prime  12699  zeo  12704  fnn0ind  12717  zindd  12719  btwnz  12721  lbzbi  12978  xrub  13354  elfznelfzo  13811  fvf1tp  13829  addmodlteq  13987  facwordi  14328  fiinfnf1o  14389  hashclb  14397  hashdom  14418  hashf1lem2  14495  seqcoll  14503  brfi1indALT  14549  ccatalpha  14631  pfxccatin12lem2a  14765  limsupbnd2  15519  rlimdm  15587  o1of2  15649  rlimno1  15690  isercoll  15704  caurcvg2  15714  caucvgb  15716  serf0  15717  zsum  15754  fsum2dlem  15806  fsum2d  15807  fsumabs  15837  fsumrlim  15847  fsumo1  15848  fsumiun  15857  zprod  15973  fprod2dlem  16016  fprod2d  16017  odd2np1  16378  ndvdssub  16446  dfgcd2  16583  nprm  16725  maxprmfct  16746  rpexp  16759  pc2dvds  16917  pcfac  16937  unbenlem  16946  4sqlem12  16994  4sqlem17  16999  vdwlem13  17031  prmlem0  17143  mreiincl  17639  sscfn1  17861  initoid  18046  termoid  18047  funcestrcsetclem8  18192  funcsetcestrclem8  18207  pospo  18390  cnvpsb  18624  dirtr  18647  mulgaddcom  19116  mulginvcom  19117  gaass  19315  cntz2ss  19353  elsymgbas  19391  symgfix2  19434  pmtrfrn  19476  psgnran  19533  odmulg  19574  odhash3  19594  sylow2alem1  19635  sylow2alem2  19636  pj1eu  19714  efgs1b  19754  efgsfo  19757  efgredlemc  19763  efgredeu  19770  frgpuptinv  19789  lt6abl  19913  ghmcyg  19914  ablfac1eulem  20092  pgpfac1lem5  20099  ablsimpgfindlem1  20127  ringinvnz1ne0  20297  irredmul  20429  rnghmsscmap2  20629  rnghmsscmap  20630  rhmsscmap2  20658  rhmsscmap  20659  acsfn1p  20800  lspextmo  21055  lspsncv0  21148  pzriprnglem12  21503  psgnghm  21598  mplcoe1  22055  mplcoe5  22058  evlseu  22107  mhpsclcl  22151  mdetunilem7  22624  mdetunilem9  22626  chcoeffeq  22892  cnindis  23300  lmss  23306  lmcls  23310  lmcnp  23312  hausnei  23336  cmpsub  23408  tgcmp  23409  fiuncmp  23412  cmpfi  23416  bwth  23418  1stcrest  23461  2ndcdisj  23464  1stccnp  23470  comppfsc  23540  1stckgenlem  23561  txcls  23612  txcn  23634  txlm  23656  tx1stc  23658  xkococn  23668  hmphdis  23804  ptcmpfi  23821  isfild  23866  fgss2  23882  filconn  23891  trfil2  23895  ufileu  23927  filufint  23928  elfm2  23956  flftg  24004  fclssscls  24026  fclscf  24033  ufilcmp  24040  cnpfcf  24049  alexsubb  24054  alexsubALTlem4  24058  alexsubALT  24059  qustgpopn  24128  tsmsxp  24163  isust  24212  xmettri2  24350  blin2  24439  setsmstopn  24490  met2ndc  24536  metcnp3  24553  tngtopn  24671  reconnlem2  24849  xrge0tsms  24856  fsumcn  24894  bndth  24990  iscmet3lem2  25326  iscmet3  25327  ivthlem1  25486  ivthlem2  25487  ivthlem3  25488  ovolfiniun  25536  volfiniun  25582  ioombl1lem4  25596  ismbf3d  25689  mbfi1flimlem  25757  itg2seq  25777  itgfsum  25862  ellimc3  25914  dvmptfsum  26013  c1liplem1  26035  plypf1  26251  plydivex  26339  aannenlem1  26370  ulmval  26423  ulmcau  26438  ulmbdd  26441  ulmcn  26442  ulmdvlem3  26445  sineq0  26566  efopn  26700  cxpeq  26800  logbgcd1irr  26837  rlimcnp  27008  xrlimcnp  27011  lgsdir2lem2  27370  lgsne0  27379  2lgsoddprm  27460  2sqlem6  27467  2sqlem10  27472  2sqreunnltblem  27495  sltval2  27701  noetasuplem4  27781  conway  27844  madebdayim  27926  addsass  28038  zs12bday  28424  axcontlem2  28980  uhgr0vb  29089  uvtx01vtx  29414  uvtxupgrres  29425  fusgrn0degnn0  29517  finsumvtxdg2size  29568  cusgrm1rusgr  29600  wlkv0  29669  wlklenvclwlk  29673  uspgrn2crct  29828  frrusgrord  30360  numclwwlk1lem2fo  30377  isgrpo  30516  grpoidinvlem3  30525  vcdi  30584  vcdir  30585  vcass  30586  nvs  30682  nvtri  30689  blocnilem  30823  chintcli  31350  hsupss  31360  shlej1  31379  elspansn4  31592  spansncvi  31671  hoaddsub  31835  lnopl  31933  lnfnl  31950  riesz4i  32082  pjnormssi  32187  pj3si  32226  stlei  32259  stcltr2i  32294  dmdmd  32319  dmdbr5  32327  mdslmd1lem2  32345  atssma  32397  atcvatlem  32404  chirredlem1  32409  atcvat4i  32416  mdsymlem2  32423  mdsymlem6  32427  sumdmdlem2  32438  cdjreui  32451  elimifd  32556  disjxpin  32601  unifi3  32724  xrge0infss  32764  expgt0b  32818  xrge0tsmsd  33065  gsumle  33101  gsumvsca1  33232  gsumvsca2  33233  lmxrge0  33951  ismeas  34200  eulerpartlemb  34370  bnj849  34939  bnj1110  34996  srcmpltd  35094  swrdrevpfx  35122  cusgredgex2  35128  subgrwlk  35137  cusgr3cyclex  35141  umgr2cycllem  35145  umgr2cycl  35146  connpconn  35240  cvmseu  35281  cvmliftlem15  35303  cvmlift2lem1  35307  cvmlift2lem12  35319  satfv0fun  35376  satffunlem  35406  mclsind  35575  r1peuqusdeg1  35648  dfon2lem3  35786  dfon2lem4  35787  dfon2lem6  35789  dfon2lem8  35791  dfon2lem9  35792  hbntg  35806  cgrdegen  36005  funtransport  36032  ifscgr  36045  cgrxfr  36056  brofs2  36078  brifs2  36079  idinside  36085  btwnconn1lem7  36094  btwnconn1lem11  36098  btwnconn1lem12  36099  btwnconn1lem14  36101  broutsideof2  36123  btwnoutside  36126  outsideoftr  36130  in-ax8  36225  ss-ax8  36226  finminlem  36319  ntruni  36328  neibastop1  36360  ontgval  36432  ordtop  36437  ordcmp  36448  onint1  36450  bj-ax12w  36678  axc11n11r  36684  bj-ax12v3  36686  bj-nnfan  36749  bj-nnfand  36750  bj-nnflemea  36766  bj-19.42t  36774  bj-sbft  36776  bj-hbaeb2  36819  bj-spcimdv  36896  bj-spcimdvv  36897  bj-sngltag  36984  bj-xtagex  36990  bj-0int  37102  bj-ismooredr  37110  bj-inftyexpiinj  37210  nlpfvineqsn  37410  wl-ax13lem1  37495  wl-speqv  37523  wl-sbcom2d  37562  wl-ax11-lem3  37588  wl-ax11-lem8  37593  tan2h  37619  ptrest  37626  poimirlem20  37647  poimirlem22  37649  poimirlem26  37653  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  heicant  37662  voliunnfl  37671  volsupnfl  37672  itg2addnclem2  37679  itg2addnc  37681  itg2gt0cn  37682  ftc2nc  37709  filbcmb  37747  sdclem2  37749  seqpo  37754  nninfnub  37758  neificl  37760  prdstotbnd  37801  cnpwstotbnd  37804  heibor1lem  37816  heibor  37828  bfplem2  37830  opidonOLD  37859  exidu1  37863  grpokerinj  37900  rngoideu  37910  rngodi  37911  rngodir  37912  rngmgmbs4  37938  divrngidl  38035  prnc  38074  eqvrelqsel  38617  erimeq2  38679  prter2  38882  ax4fromc4  38895  hbae-o  38904  dvelimf-o  38930  ax12indn  38944  ax12inda2  38948  ax12a2-o  38951  l1cvpat  39055  atcvrj0  39430  pmaple  39763  paddasslem5  39826  pclfinN  39902  osumcllem11N  39968  pexmidlem8N  39979  dvheveccl  41114  dihord6apre  41258  lpolconN  41489  lcmineqlem1  42030  oexpreposd  42357  sn-it0e0  42445  cnreeu  42500  eu6w  42686  isnacs3  42721  pellexlem5  42844  pellex  42846  jm2.18  43000  jm2.15nn0  43015  jm2.16nn0  43016  dford3lem2  43039  ttac  43048  onexomgt  43253  onexoegt  43256  omabs2  43345  omcl3g  43347  tfsconcat0b  43359  naddgeoa  43407  safesnsupfiss  43428  rp-isfinite5  43530  cnvssb  43599  clcnvlem  43636  iunrelexpuztr  43732  rfovcnvf1od  44017  ntrrn  44135  nzss  44336  pm11.71  44416  axc11next  44425  hbntal  44573  eel2122old  44738  relwf  44984  modelaxreplem1  44995  ssclaxsep  44999  wfac8prim  45019  fsetsnf1  47064  2reu8i  47125  afvelima  47179  rlimdmafv  47189  rlimdmafv2  47270  elsprel  47462  sfprmdvdsmersenne  47590  perfectALTVlem2  47709  fpprwppr  47726  isuspgrim0lem  47871  uhgrimisgrgric  47899  gpgcubic  48035  gpg5nbgr3star  48037  copisnmnd  48085  funcringcsetcALTV2lem8  48213  funcringcsetclem8ALTV  48236  lindslinindsimp2lem5  48379  nn0sumshdig  48544  prelrrx2b  48635  itscnhlc0yqe  48680  iscnrm3lem2  48832  spd  49197  setrec1lem4  49209  setrec2fun  49211  aacllem  49320