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  3155  spcimgfi1OLD  3505  rr19.28v  3625  moeq3  3674  reuimrmo  3707  sbeqalb  3807  csbexg  5252  ralxfrd  5350  ralxfrd2  5354  ralxfrALT  5357  copsexgw  5437  copsexg  5438  pwssun  5515  somo  5570  ssrel  5730  relssres  5977  dmsnopg  6166  dfco2a  6199  dfpo2  6248  frpoinsg  6295  tz7.7  6337  ordunidif  6361  suctr  6399  trsucss  6401  suc11  6420  imadif  6570  dffv2  6922  fvmptd3f  6949  fvmptnf  6956  foco2  7047  fconst5  7146  fvf1pr  7248  isores3  7276  riotaxfrd  7344  ovmpt4g  7500  ovmpos  7501  ov2gf  7502  ovmpodf  7509  sorpsscmpl  7674  abnexg  7696  onint  7730  limuni3  7792  tfisg  7794  tfis  7795  tfinds  7800  limomss  7811  peano5  7833  fo2ndf  8061  frxp  8066  xpord2pred  8085  xpord2indlem  8087  soseq  8099  suppss2  8140  suppssfv  8142  rntpos  8179  fprlem1  8240  fprresex  8250  wfr3g  8259  onfununi  8271  smofvon2  8286  smo11  8294  smoord  8295  tfrlem11  8317  tz7.44-2  8336  tz7.48lem  8370  tz7.48-1  8372  tz7.49  8374  tz7.49c  8375  omordi  8491  omord  8493  omass  8505  oneo  8506  omeulem1  8507  omopth2  8509  oewordri  8517  oeworde  8518  nnmordi  8556  nnmord  8557  omabs  8576  nnneo  8580  omsmo  8583  naddcllem  8601  qsel  8730  eceqoveq  8756  domunsncan  9001  sbthlem1  9011  2pwuninel  9056  mapen  9065  infensuc  9079  rexdif1en  9082  findcard2  9088  pssnn  9092  ssfi  9097  sucdom2  9127  php  9131  onomeneq  9138  0sdom1dom  9145  sdom1  9149  dif1ennnALT  9180  ac6sfi  9189  frfi  9190  unblem1  9197  unblem2  9198  unbnn2  9202  nnsdomgOLD  9205  xpfiOLD  9228  domunfican  9230  fiintOLD  9236  fodomfir  9237  ixpfi2  9259  finsschain  9268  marypha1lem  9342  oiexg  9446  brwdom3  9493  inf3lem2  9544  inf3lem3  9545  cantnfval2  9584  cantnflt  9587  cantnflem1  9604  cnfcom  9615  ttrclss  9635  trcl  9643  epfrs  9646  frmin  9664  frinsg  9666  frr3g  9671  frrlem15  9672  r1sdom  9689  cardsdomel  9889  carduni  9896  infpwfien  9975  carduniima  10009  dfac5  10042  dfac12r  10060  dfac12k  10061  kmlem11  10074  djuinf  10102  infxp  10127  cfsuc  10170  cfcoflem  10185  coftr  10186  infpssr  10221  fin23lem30  10255  isf32lem1  10266  isf34lem6  10293  fin1a2lem13  10325  fin1a2s  10327  axcc2lem  10349  domtriomlem  10355  axcclem  10370  ac6num  10392  zorn2lem5  10413  zorn2lem6  10414  axdclem2  10433  alephval2  10485  alephreg  10495  pwcfsdom  10496  axregndlem1  10515  axregnd  10517  axacndlem1  10520  axacndlem2  10521  axacndlem3  10522  axacndlem4  10523  axacnd  10525  gchi  10537  fpwwe2lem12  10555  canthp1  10567  gchpwdom  10583  wunfi  10634  tskwe2  10686  inar1  10688  gruen  10725  intgru  10727  indpi  10820  nqereu  10842  ltbtwnnq  10891  prnmadd  10910  genpcd  10919  prlem934  10946  ltexprlem1  10949  ltexprlem2  10950  ltexprlem7  10955  ltaprlem  10957  ltapr  10958  reclem4pr  10963  suplem2pr  10966  mulcmpblnr  10984  recexsrlem  11016  mulgt0sr  11018  supsrlem  11024  axpre-sup  11082  1re  11134  dedekindle  11298  addlsub  11554  recex  11770  nnunb  12398  0mnnnnn0  12434  prime  12575  zeo  12580  fnn0ind  12593  zindd  12595  btwnz  12597  lbzbi  12855  xrub  13232  elfznelfzo  13693  fvf1tp  13711  addmodlteq  13871  facwordi  14214  fiinfnf1o  14275  hashclb  14283  hashdom  14304  hashf1lem2  14381  seqcoll  14389  brfi1indALT  14435  ccatalpha  14518  pfxccatin12lem2a  14651  limsupbnd2  15408  rlimdm  15476  o1of2  15538  rlimno1  15579  isercoll  15593  caurcvg2  15603  caucvgb  15605  serf0  15606  zsum  15643  fsum2dlem  15695  fsum2d  15696  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  zprod  15862  fprod2dlem  15905  fprod2d  15906  odd2np1  16270  ndvdssub  16338  dfgcd2  16475  nprm  16617  maxprmfct  16638  rpexp  16651  pc2dvds  16809  pcfac  16829  unbenlem  16838  4sqlem12  16886  4sqlem17  16891  vdwlem13  16923  prmlem0  17035  mreiincl  17516  sscfn1  17742  initoid  17926  termoid  17927  funcestrcsetclem8  18071  funcsetcestrclem8  18086  pospo  18267  cnvpsb  18503  dirtr  18526  mulgaddcom  18995  mulginvcom  18996  gaass  19194  cntz2ss  19232  elsymgbas  19271  symgfix2  19313  pmtrfrn  19355  psgnran  19412  odmulg  19453  odhash3  19473  sylow2alem1  19514  sylow2alem2  19515  pj1eu  19593  efgs1b  19633  efgsfo  19636  efgredlemc  19642  efgredeu  19649  frgpuptinv  19668  lt6abl  19792  ghmcyg  19793  ablfac1eulem  19971  pgpfac1lem5  19978  ablsimpgfindlem1  20006  gsumle  20042  ringinvnz1ne0  20203  irredmul  20332  rnghmsscmap2  20532  rnghmsscmap  20533  rhmsscmap2  20561  rhmsscmap  20562  acsfn1p  20702  lspextmo  20978  lspsncv0  21071  pzriprnglem12  21417  psgnghm  21505  mplcoe1  21960  mplcoe5  21963  evlseu  22006  mhpsclcl  22050  mdetunilem7  22521  mdetunilem9  22523  chcoeffeq  22789  cnindis  23195  lmss  23201  lmcls  23205  lmcnp  23207  hausnei  23231  cmpsub  23303  tgcmp  23304  fiuncmp  23307  cmpfi  23311  bwth  23313  1stcrest  23356  2ndcdisj  23359  1stccnp  23365  comppfsc  23435  1stckgenlem  23456  txcls  23507  txcn  23529  txlm  23551  tx1stc  23553  xkococn  23563  hmphdis  23699  ptcmpfi  23716  isfild  23761  fgss2  23777  filconn  23786  trfil2  23790  ufileu  23822  filufint  23823  elfm2  23851  flftg  23899  fclssscls  23921  fclscf  23928  ufilcmp  23935  cnpfcf  23944  alexsubb  23949  alexsubALTlem4  23953  alexsubALT  23954  qustgpopn  24023  tsmsxp  24058  isust  24107  xmettri2  24244  blin2  24333  setsmstopn  24382  met2ndc  24427  metcnp3  24444  tngtopn  24554  reconnlem2  24732  xrge0tsms  24739  fsumcn  24777  bndth  24873  iscmet3lem2  25208  iscmet3  25209  ivthlem1  25368  ivthlem2  25369  ivthlem3  25370  ovolfiniun  25418  volfiniun  25464  ioombl1lem4  25478  ismbf3d  25571  mbfi1flimlem  25639  itg2seq  25659  itgfsum  25744  ellimc3  25796  dvmptfsum  25895  c1liplem1  25917  plypf1  26133  plydivex  26221  aannenlem1  26252  ulmval  26305  ulmcau  26320  ulmbdd  26323  ulmcn  26324  ulmdvlem3  26327  sineq0  26449  efopn  26583  cxpeq  26683  logbgcd1irr  26720  rlimcnp  26891  xrlimcnp  26894  lgsdir2lem2  27253  lgsne0  27262  2lgsoddprm  27343  2sqlem6  27350  2sqlem10  27355  2sqreunnltblem  27378  sltval2  27584  noetasuplem4  27664  conway  27728  madebdayim  27820  addsass  27935  onscutlt  28188  onsiso  28192  bdayn0p1  28281  zs12zodd  28377  zs12bday  28379  axcontlem2  28928  uhgr0vb  29035  uvtx01vtx  29360  uvtxupgrres  29371  fusgrn0degnn0  29463  finsumvtxdg2size  29514  cusgrm1rusgr  29546  wlkv0  29613  wlklenvclwlk  29617  uspgrn2crct  29771  frrusgrord  30303  numclwwlk1lem2fo  30320  isgrpo  30459  grpoidinvlem3  30468  vcdi  30527  vcdir  30528  vcass  30529  nvs  30625  nvtri  30632  blocnilem  30766  chintcli  31293  hsupss  31303  shlej1  31322  elspansn4  31535  spansncvi  31614  hoaddsub  31778  lnopl  31876  lnfnl  31893  riesz4i  32025  pjnormssi  32130  pj3si  32169  stlei  32202  stcltr2i  32237  dmdmd  32262  dmdbr5  32270  mdslmd1lem2  32288  atssma  32340  atcvatlem  32347  chirredlem1  32352  atcvat4i  32359  mdsymlem2  32366  mdsymlem6  32370  sumdmdlem2  32381  cdjreui  32394  elimifd  32505  disjxpin  32550  unifi3  32669  xrge0infss  32716  expgt0b  32774  xrge0tsmsd  33028  gsumvsca1  33178  gsumvsca2  33179  lmxrge0  33918  ismeas  34165  eulerpartlemb  34335  bnj849  34891  bnj1110  34948  srcmpltd  35046  swrdrevpfx  35089  cusgredgex2  35095  subgrwlk  35104  cusgr3cyclex  35108  umgr2cycllem  35112  umgr2cycl  35113  connpconn  35207  cvmseu  35248  cvmliftlem15  35270  cvmlift2lem1  35274  cvmlift2lem12  35286  satfv0fun  35343  satffunlem  35373  mclsind  35542  r1peuqusdeg1  35615  dfon2lem3  35758  dfon2lem4  35759  dfon2lem6  35761  dfon2lem8  35763  dfon2lem9  35764  hbntg  35778  cgrdegen  35977  funtransport  36004  ifscgr  36017  cgrxfr  36028  brofs2  36050  brifs2  36051  idinside  36057  btwnconn1lem7  36066  btwnconn1lem11  36070  btwnconn1lem12  36071  btwnconn1lem14  36073  broutsideof2  36095  btwnoutside  36098  outsideoftr  36102  in-ax8  36197  ss-ax8  36198  finminlem  36291  ntruni  36300  neibastop1  36332  ontgval  36404  ordtop  36409  ordcmp  36420  onint1  36422  bj-ax12w  36650  axc11n11r  36656  bj-ax12v3  36658  bj-nnfan  36721  bj-nnfand  36722  bj-nnflemea  36738  bj-19.42t  36746  bj-sbft  36748  bj-hbaeb2  36791  bj-spcimdv  36868  bj-spcimdvv  36869  bj-sngltag  36956  bj-xtagex  36962  bj-0int  37074  bj-ismooredr  37082  bj-inftyexpiinj  37182  nlpfvineqsn  37382  wl-ax13lem1  37467  wl-speqv  37495  wl-sbcom2d  37534  wl-ax11-lem3  37560  wl-ax11-lem8  37565  tan2h  37591  ptrest  37598  poimirlem20  37619  poimirlem22  37621  poimirlem26  37625  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  heicant  37634  voliunnfl  37643  volsupnfl  37644  itg2addnclem2  37651  itg2addnc  37653  itg2gt0cn  37654  ftc2nc  37681  filbcmb  37719  sdclem2  37721  seqpo  37726  nninfnub  37730  neificl  37732  prdstotbnd  37773  cnpwstotbnd  37776  heibor1lem  37788  heibor  37800  bfplem2  37802  opidonOLD  37831  exidu1  37835  grpokerinj  37872  rngoideu  37882  rngodi  37883  rngodir  37884  rngmgmbs4  37910  divrngidl  38007  prnc  38046  eqvrelqsel  38592  erimeq2  38655  prter2  38859  ax4fromc4  38872  hbae-o  38881  dvelimf-o  38907  ax12indn  38921  ax12inda2  38925  ax12a2-o  38928  l1cvpat  39032  atcvrj0  39407  pmaple  39740  paddasslem5  39803  pclfinN  39879  osumcllem11N  39945  pexmidlem8N  39956  dvheveccl  41091  dihord6apre  41235  lpolconN  41466  lcmineqlem1  42002  oexpreposd  42295  sn-it0e0  42389  cnreeu  42463  eu6w  42649  isnacs3  42683  pellexlem5  42806  pellex  42808  jm2.18  42961  jm2.15nn0  42976  jm2.16nn0  42977  dford3lem2  43000  ttac  43009  onexomgt  43214  onexoegt  43217  omabs2  43305  omcl3g  43307  tfsconcat0b  43319  naddgeoa  43367  safesnsupfiss  43388  rp-isfinite5  43490  cnvssb  43559  clcnvlem  43596  iunrelexpuztr  43692  rfovcnvf1od  43977  ntrrn  44095  nzss  44290  pm11.71  44370  axc11next  44379  hbntal  44527  eel2122old  44691  relwf  44941  modelaxreplem1  44952  ssclaxsep  44956  wfac8prim  44976  fsetsnf1  47037  2reu8i  47098  afvelima  47152  rlimdmafv  47162  rlimdmafv2  47243  elsprel  47460  sfprmdvdsmersenne  47588  perfectALTVlem2  47707  fpprwppr  47724  uhgrimedgi  47875  isuspgrim0lem  47878  uhgrimisgrgric  47916  gpgcubic  48064  gpg5nbgr3star  48066  pgnioedg1  48093  pgnioedg2  48094  pgnioedg3  48095  pgnioedg4  48096  pgnioedg5  48097  copisnmnd  48154  funcringcsetcALTV2lem8  48282  funcringcsetclem8ALTV  48305  lindslinindsimp2lem5  48448  nn0sumshdig  48609  prelrrx2b  48700  itscnhlc0yqe  48745  iscnrm3lem2  48920  diag1f1lem  49292  spd  49664  setrec1lem4  49676  setrec2fun  49678  aacllem  49787