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  951  pm2.36  971  pm4.79  1005  ecased  1035  alrimdh  1863  stdpc5v  1938  19.37imv  1947  ax12w  2134  ax13dgen2  2139  ax12v  2179  spsd  2188  nf5r  2195  axc4  2320  equs5eALT  2365  ax13lem1  2372  nfeqf  2379  hbae  2429  ax12vALT  2467  2ax6elem  2468  sb1  2476  euimmo  2609  necon2ad  2940  necon4ad  2944  r19.37v  3160  spcimgfi1OLD  3514  rr19.28v  3634  moeq3  3683  reuimrmo  3716  sbeqalb  3816  csbexg  5265  ralxfrd  5363  ralxfrd2  5367  ralxfrALT  5370  copsexgw  5450  copsexg  5451  pwssun  5530  somo  5585  ssrel  5745  ssrelOLD  5746  relssres  5993  dmsnopg  6186  dfco2a  6219  dfpo2  6269  frpoinsg  6316  tz7.7  6358  ordunidif  6382  suctr  6420  trsucss  6422  suc11  6441  imadif  6600  dffv2  6956  fvmptd3f  6983  fvmptnf  6990  foco2  7081  fconst5  7180  fvf1pr  7282  isores3  7310  riotaxfrd  7378  ovmpt4g  7536  ovmpos  7537  ov2gf  7538  ovmpodf  7545  sorpsscmpl  7710  abnexg  7732  onint  7766  limuni3  7828  tfisg  7830  tfis  7831  tfinds  7836  limomss  7847  peano5  7869  fo2ndf  8100  frxp  8105  xpord2pred  8124  xpord2indlem  8126  soseq  8138  suppss2  8179  suppssfv  8181  rntpos  8218  fprlem1  8279  fprresex  8289  wfr3g  8298  onfununi  8310  smofvon2  8325  smo11  8333  smoord  8334  tfrlem11  8356  tz7.44-2  8375  tz7.48lem  8409  tz7.48-1  8411  tz7.49  8413  tz7.49c  8414  omordi  8530  omord  8532  omass  8544  oneo  8545  omeulem1  8546  omopth2  8548  oewordri  8556  oeworde  8557  nnmordi  8595  nnmord  8596  omabs  8615  nnneo  8619  omsmo  8622  naddcllem  8640  qsel  8769  eceqoveq  8795  domunsncan  9041  sbthlem1  9051  2pwuninel  9096  mapen  9105  infensuc  9119  rexdif1en  9122  findcard2  9128  pssnn  9132  ssfi  9137  sucdom2  9167  php  9171  onomeneq  9178  0sdom1dom  9185  sdom1  9189  dif1ennnALT  9222  ac6sfi  9231  frfi  9232  unblem1  9239  unblem2  9240  unbnn2  9244  nnsdomgOLD  9247  xpfiOLD  9270  domunfican  9272  fiintOLD  9278  fodomfir  9279  ixpfi2  9301  finsschain  9310  marypha1lem  9384  oiexg  9488  brwdom3  9535  inf3lem2  9582  inf3lem3  9583  cantnfval2  9622  cantnflt  9625  cantnflem1  9642  cnfcom  9653  ttrclss  9673  trcl  9681  epfrs  9684  frmin  9702  frinsg  9704  frr3g  9709  frrlem15  9710  r1sdom  9727  cardsdomel  9927  carduni  9934  pr2neOLD  9958  infpwfien  10015  carduniima  10049  dfac5  10082  dfac12r  10100  dfac12k  10101  kmlem11  10114  djuinf  10142  infxp  10167  cfsuc  10210  cfcoflem  10225  coftr  10226  infpssr  10261  fin23lem30  10295  isf32lem1  10306  isf34lem6  10333  fin1a2lem13  10365  fin1a2s  10367  axcc2lem  10389  domtriomlem  10395  axcclem  10410  ac6num  10432  zorn2lem5  10453  zorn2lem6  10454  axdclem2  10473  alephval2  10525  alephreg  10535  pwcfsdom  10536  axregndlem1  10555  axregnd  10557  axacndlem1  10560  axacndlem2  10561  axacndlem3  10562  axacndlem4  10563  axacnd  10565  gchi  10577  fpwwe2lem12  10595  canthp1  10607  gchpwdom  10623  wunfi  10674  tskwe2  10726  inar1  10728  gruen  10765  intgru  10767  indpi  10860  nqereu  10882  ltbtwnnq  10931  prnmadd  10950  genpcd  10959  prlem934  10986  ltexprlem1  10989  ltexprlem2  10990  ltexprlem7  10995  ltaprlem  10997  ltapr  10998  reclem4pr  11003  suplem2pr  11006  mulcmpblnr  11024  recexsrlem  11056  mulgt0sr  11058  supsrlem  11064  axpre-sup  11122  1re  11174  dedekindle  11338  addlsub  11594  recex  11810  nnunb  12438  0mnnnnn0  12474  prime  12615  zeo  12620  fnn0ind  12633  zindd  12635  btwnz  12637  lbzbi  12895  xrub  13272  elfznelfzo  13733  fvf1tp  13751  addmodlteq  13911  facwordi  14254  fiinfnf1o  14315  hashclb  14323  hashdom  14344  hashf1lem2  14421  seqcoll  14429  brfi1indALT  14475  ccatalpha  14558  pfxccatin12lem2a  14692  limsupbnd2  15449  rlimdm  15517  o1of2  15579  rlimno1  15620  isercoll  15634  caurcvg2  15644  caucvgb  15646  serf0  15647  zsum  15684  fsum2dlem  15736  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fsumiun  15787  zprod  15903  fprod2dlem  15946  fprod2d  15947  odd2np1  16311  ndvdssub  16379  dfgcd2  16516  nprm  16658  maxprmfct  16679  rpexp  16692  pc2dvds  16850  pcfac  16870  unbenlem  16879  4sqlem12  16927  4sqlem17  16932  vdwlem13  16964  prmlem0  17076  mreiincl  17557  sscfn1  17779  initoid  17963  termoid  17964  funcestrcsetclem8  18108  funcsetcestrclem8  18123  pospo  18304  cnvpsb  18538  dirtr  18561  mulgaddcom  19030  mulginvcom  19031  gaass  19229  cntz2ss  19267  elsymgbas  19304  symgfix2  19346  pmtrfrn  19388  psgnran  19445  odmulg  19486  odhash3  19506  sylow2alem1  19547  sylow2alem2  19548  pj1eu  19626  efgs1b  19666  efgsfo  19669  efgredlemc  19675  efgredeu  19682  frgpuptinv  19701  lt6abl  19825  ghmcyg  19826  ablfac1eulem  20004  pgpfac1lem5  20011  ablsimpgfindlem1  20039  ringinvnz1ne0  20209  irredmul  20338  rnghmsscmap2  20538  rnghmsscmap  20539  rhmsscmap2  20567  rhmsscmap  20568  acsfn1p  20708  lspextmo  20963  lspsncv0  21056  pzriprnglem12  21402  psgnghm  21489  mplcoe1  21944  mplcoe5  21947  evlseu  21990  mhpsclcl  22034  mdetunilem7  22505  mdetunilem9  22507  chcoeffeq  22773  cnindis  23179  lmss  23185  lmcls  23189  lmcnp  23191  hausnei  23215  cmpsub  23287  tgcmp  23288  fiuncmp  23291  cmpfi  23295  bwth  23297  1stcrest  23340  2ndcdisj  23343  1stccnp  23349  comppfsc  23419  1stckgenlem  23440  txcls  23491  txcn  23513  txlm  23535  tx1stc  23537  xkococn  23547  hmphdis  23683  ptcmpfi  23700  isfild  23745  fgss2  23761  filconn  23770  trfil2  23774  ufileu  23806  filufint  23807  elfm2  23835  flftg  23883  fclssscls  23905  fclscf  23912  ufilcmp  23919  cnpfcf  23928  alexsubb  23933  alexsubALTlem4  23937  alexsubALT  23938  qustgpopn  24007  tsmsxp  24042  isust  24091  xmettri2  24228  blin2  24317  setsmstopn  24366  met2ndc  24411  metcnp3  24428  tngtopn  24538  reconnlem2  24716  xrge0tsms  24723  fsumcn  24761  bndth  24857  iscmet3lem2  25192  iscmet3  25193  ivthlem1  25352  ivthlem2  25353  ivthlem3  25354  ovolfiniun  25402  volfiniun  25448  ioombl1lem4  25462  ismbf3d  25555  mbfi1flimlem  25623  itg2seq  25643  itgfsum  25728  ellimc3  25780  dvmptfsum  25879  c1liplem1  25901  plypf1  26117  plydivex  26205  aannenlem1  26236  ulmval  26289  ulmcau  26304  ulmbdd  26307  ulmcn  26308  ulmdvlem3  26311  sineq0  26433  efopn  26567  cxpeq  26667  logbgcd1irr  26704  rlimcnp  26875  xrlimcnp  26878  lgsdir2lem2  27237  lgsne0  27246  2lgsoddprm  27327  2sqlem6  27334  2sqlem10  27339  2sqreunnltblem  27362  sltval2  27568  noetasuplem4  27648  conway  27711  madebdayim  27799  addsass  27912  onscutlt  28165  onsiso  28169  bdayn0p1  28258  zs12bday  28343  axcontlem2  28892  uhgr0vb  28999  uvtx01vtx  29324  uvtxupgrres  29335  fusgrn0degnn0  29427  finsumvtxdg2size  29478  cusgrm1rusgr  29510  wlkv0  29579  wlklenvclwlk  29583  uspgrn2crct  29738  frrusgrord  30270  numclwwlk1lem2fo  30287  isgrpo  30426  grpoidinvlem3  30435  vcdi  30494  vcdir  30495  vcass  30496  nvs  30592  nvtri  30599  blocnilem  30733  chintcli  31260  hsupss  31270  shlej1  31289  elspansn4  31502  spansncvi  31581  hoaddsub  31745  lnopl  31843  lnfnl  31860  riesz4i  31992  pjnormssi  32097  pj3si  32136  stlei  32169  stcltr2i  32204  dmdmd  32229  dmdbr5  32237  mdslmd1lem2  32255  atssma  32307  atcvatlem  32314  chirredlem1  32319  atcvat4i  32326  mdsymlem2  32333  mdsymlem6  32337  sumdmdlem2  32348  cdjreui  32361  elimifd  32472  disjxpin  32517  unifi3  32636  xrge0infss  32683  expgt0b  32741  xrge0tsmsd  33002  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  lmxrge0  33942  ismeas  34189  eulerpartlemb  34359  bnj849  34915  bnj1110  34972  srcmpltd  35070  swrdrevpfx  35104  cusgredgex2  35110  subgrwlk  35119  cusgr3cyclex  35123  umgr2cycllem  35127  umgr2cycl  35128  connpconn  35222  cvmseu  35263  cvmliftlem15  35285  cvmlift2lem1  35289  cvmlift2lem12  35301  satfv0fun  35358  satffunlem  35388  mclsind  35557  r1peuqusdeg1  35630  dfon2lem3  35773  dfon2lem4  35774  dfon2lem6  35776  dfon2lem8  35778  dfon2lem9  35779  hbntg  35793  cgrdegen  35992  funtransport  36019  ifscgr  36032  cgrxfr  36043  brofs2  36065  brifs2  36066  idinside  36072  btwnconn1lem7  36081  btwnconn1lem11  36085  btwnconn1lem12  36086  btwnconn1lem14  36088  broutsideof2  36110  btwnoutside  36113  outsideoftr  36117  in-ax8  36212  ss-ax8  36213  finminlem  36306  ntruni  36315  neibastop1  36347  ontgval  36419  ordtop  36424  ordcmp  36435  onint1  36437  bj-ax12w  36665  axc11n11r  36671  bj-ax12v3  36673  bj-nnfan  36736  bj-nnfand  36737  bj-nnflemea  36753  bj-19.42t  36761  bj-sbft  36763  bj-hbaeb2  36806  bj-spcimdv  36883  bj-spcimdvv  36884  bj-sngltag  36971  bj-xtagex  36977  bj-0int  37089  bj-ismooredr  37097  bj-inftyexpiinj  37197  nlpfvineqsn  37397  wl-ax13lem1  37482  wl-speqv  37510  wl-sbcom2d  37549  wl-ax11-lem3  37575  wl-ax11-lem8  37580  tan2h  37606  ptrest  37613  poimirlem20  37634  poimirlem22  37636  poimirlem26  37640  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  heicant  37649  voliunnfl  37658  volsupnfl  37659  itg2addnclem2  37666  itg2addnc  37668  itg2gt0cn  37669  ftc2nc  37696  filbcmb  37734  sdclem2  37736  seqpo  37741  nninfnub  37745  neificl  37747  prdstotbnd  37788  cnpwstotbnd  37791  heibor1lem  37803  heibor  37815  bfplem2  37817  opidonOLD  37846  exidu1  37850  grpokerinj  37887  rngoideu  37897  rngodi  37898  rngodir  37899  rngmgmbs4  37925  divrngidl  38022  prnc  38061  eqvrelqsel  38607  erimeq2  38670  prter2  38874  ax4fromc4  38887  hbae-o  38896  dvelimf-o  38922  ax12indn  38936  ax12inda2  38940  ax12a2-o  38943  l1cvpat  39047  atcvrj0  39422  pmaple  39755  paddasslem5  39818  pclfinN  39894  osumcllem11N  39960  pexmidlem8N  39971  dvheveccl  41106  dihord6apre  41250  lpolconN  41481  lcmineqlem1  42017  oexpreposd  42310  sn-it0e0  42404  cnreeu  42478  eu6w  42664  isnacs3  42698  pellexlem5  42821  pellex  42823  jm2.18  42977  jm2.15nn0  42992  jm2.16nn0  42993  dford3lem2  43016  ttac  43025  onexomgt  43230  onexoegt  43233  omabs2  43321  omcl3g  43323  tfsconcat0b  43335  naddgeoa  43383  safesnsupfiss  43404  rp-isfinite5  43506  cnvssb  43575  clcnvlem  43612  iunrelexpuztr  43708  rfovcnvf1od  43993  ntrrn  44111  nzss  44306  pm11.71  44386  axc11next  44395  hbntal  44543  eel2122old  44707  relwf  44957  modelaxreplem1  44968  ssclaxsep  44972  wfac8prim  44992  fsetsnf1  47053  2reu8i  47114  afvelima  47168  rlimdmafv  47178  rlimdmafv2  47259  elsprel  47476  sfprmdvdsmersenne  47604  perfectALTVlem2  47723  fpprwppr  47740  uhgrimedgi  47890  isuspgrim0lem  47893  uhgrimisgrgric  47931  gpgcubic  48070  gpg5nbgr3star  48072  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  copisnmnd  48157  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  lindslinindsimp2lem5  48451  nn0sumshdig  48612  prelrrx2b  48703  itscnhlc0yqe  48748  iscnrm3lem2  48923  diag1f1lem  49295  spd  49667  setrec1lem4  49679  setrec2fun  49681  aacllem  49790