Theorem syl5 35

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 32	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 33	1 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl56  37  syl2im  41  imim12i  63  pm2.86d  109  con2d  135  con3d  153  nsyli  158  biimtrid  245  biimtrrid  246  imbitrid  247  adantld  496  adantrd  497  impel  515  mpan9  516  pm4.72  964  pm2.36  985  pm4.79  1021  ecased  1051  alrimdh  1896  stdpc5v  1971  19.37imv  1980  ax12w  2170  ax13dgen2  2175  ax12v  2214  spsd  2224  nf5r  2231  axc4  2352  equs5eALT  2397  ax13lem1  2404  nfeqf  2411  hbae  2461  ax12vALT  2499  2ax6elem  2500  sb1  2508  euimmo  2642  necon2ad  2971  necon4ad  2975  r19.37v  3189  rr19.28v  3622  moeq3  3670  reuimrmo  3703  sbeqalb  3801  srcmpltd  4432  replem  5241  csbexg  5264  ralxfrd  5370  ralxfrd2  5374  ralxfrALT  5377  copsexgwOLD  5461  copsexg  5462  pwssun  5543  somo  5598  ssrel  5759  relssres  6011  dfrn7  6066  dmsnopg  6213  dfco2a  6246  dfpo2  6298  frpoinsg  6345  tz7.7  6387  ordunidif  6412  suctr  6450  trsucss  6452  suc11  6471  imadif  6622  dffv2  6978  fvmptd3f  7007  fvmptnf  7014  foco2  7107  fconst5  7210  fvf1pr  7313  isores3  7341  riotaxfrd  7409  ovmpt4g  7565  ovmpos  7566  ov2gf  7567  ovmpodf  7574  sorpsscmpl  7748  abnexg  7768  onint  7802  limuni3  7861  tfisg  7863  tfis  7864  tfinds  7869  limomss  7880  peano5  7903  fo2ndf  8130  frxp  8136  xpord2pred  8155  xpord2indlem  8157  soseq  8169  suppss2  8210  suppssfv  8212  rntpos  8249  fprlem1  8311  fprresex  8321  wfr3g  8330  onfununi  8342  smofvon2  8357  smo11  8365  smoord  8366  tfrlem11  8389  tz7.44-2  8408  tz7.48lemOLD  8444  tz7.48-1  8446  tz7.49  8448  tz7.49c  8449  omordi  8567  omord  8569  omass  8581  oneo  8582  omeulem1  8583  omopth2  8585  oewordri  8594  oeworde  8595  nnmordi  8633  nnmord  8634  omabs  8653  nnneo  8657  omsmo  8660  naddcllem  8678  qsel  8810  eceqoveq  8836  domunsncan  9089  sbthlem1  9099  2pwuninel  9144  mapen  9153  infensuc  9167  rexdif1en  9169  findcard2  9173  pssnn  9177  ssfi  9181  sucdom2  9211  php  9215  onomeneq  9222  0sdom1dom  9230  sdom1  9234  dif1ennnALT  9261  ac6sfi  9268  frfi  9269  unblem1  9277  unblem2  9278  unbnn2  9282  domunfican  9306  fodomfir  9312  ixpfi2  9332  finsschain  9341  unifi3  9344  marypha1lem  9418  oiexg  9522  brwdom3  9569  inf3lem2  9623  inf3lem3  9624  cantnfval2  9663  cantnflt  9666  cantnflem1  9683  cnfcom  9694  ttrclss  9714  trcl  9722  epfrs  9725  frmin  9746  frinsg  9748  frr3g  9753  frrlem15  9754  r1sdom  9774  setrec1lem4  9964  setrec2fun  9966  cardsdomel  10048  carduni  10055  infpwfien  10134  carduniima  10168  dfac5  10200  dfac12r  10218  dfac12k  10219  kmlem11  10232  djuinf  10260  infxp  10285  cfsuc  10328  cfcoflem  10343  coftr  10344  infpssr  10379  fin23lem30  10413  isf32lem1  10424  isf34lem6  10451  fin1a2lem13  10483  fin1a2s  10485  axcc2lem  10507  domtriomlem  10513  axcclem  10528  ac6num  10550  zorn2lem5  10571  zorn2lem6  10572  axdclem2  10591  alephval2  10650  alephreg  10660  pwcfsdom  10661  axregndlem1  10680  axregnd  10682  axacndlem1  10685  axacndlem2  10686  axacndlem3  10687  axacndlem4  10688  axacnd  10690  gchi  10702  fpwwe2lem12  10720  canthp1  10732  gchpwdom  10748  wunfi  10799  tskwe2  10851  inar1  10853  gruen  10890  intgru  10892  indpi  10985  nqereu  11007  ltbtwnnq  11056  prnmadd  11075  genpcd  11084  prlem934  11111  ltexprlem1  11114  ltexprlem2  11115  ltexprlem7  11120  ltaprlem  11122  ltapr  11123  reclem4pr  11128  suplem2pr  11131  mulcmpblnr  11149  recexsrlem  11181  mulgt0sr  11183  supsrlem  11189  axpre-sup  11247  1re  11301  dedekindle  11467  addlsub  11725  recex  11941  nnunb  12595  0mnnnnn0  12631  prime  12773  zeo  12778  fnn0ind  12791  zindd  12793  btwnz  12795  lbzbi  13056  xrub  13435  elfznelfzo  13901  fvf1tp  13922  addmodlteq  14082  facwordi  14426  fiinfnf1o  14487  hashclb  14495  hashdom  14516  hashf1lem2  14594  seqcoll  14602  brfi1indALT  14648  ccatalpha  14733  pfxccatin12lem2a  14869  swrdrevpfx  14911  limsupbnd2  15643  rlimdm  15711  o1of2  15773  rlimno1  15814  isercoll  15828  caurcvg2  15838  caucvgb  15840  serf0  15841  zsum  15877  fsum2dlem  15929  fsum2d  15930  fsumabs  15961  fsumrlim  15971  fsumo1  15972  fsumiun  15981  zprod  16097  fprod2dlem  16140  fprod2d  16141  odd2np1  16504  ndvdssub  16572  dfgcd2  16712  nprm  16856  maxprmfct  16878  rpexp  16891  pc2dvds  17050  pcfac  17070  unbenlem  17079  4sqlem12  17127  4sqlem17  17132  vdwlem13  17164  prmlem0  17276  mreiincl  17759  sscfn1  17985  initoid  18169  termoid  18170  funcestrcsetclem8  18314  funcsetcestrclem8  18329  pospo  18510  cnvpsb  18746  dirtr  18769  mgmidpfod  18850  mulgaddcom  19301  mulginvcom  19302  gaass  19504  cntz2ss  19542  elsymgbas  19581  symgfix2  19623  pmtrfrn  19665  psgnran  19722  odmulg  19763  odhash3  19783  sylow2alem1  19824  sylow2alem2  19825  pj1eu  19903  efgs1b  19943  efgsfo  19946  efgredlemc  19952  efgredeu  19959  frgpuptinv  19978  lt6abl  20102  ghmcyg  20103  ablfac1eulem  20281  pgpfac1lem5  20288  ablsimpgfindlem1  20316  gsumle  20352  ringinvnz1ne0  20524  irredmul  20652  rnghmsscmap2  20874  rnghmsscmap  20875  rhmsscmap2  20903  rhmsscmap  20904  acsfn1p  21049  lspextmo  21324  lspsncv0  21417  pzriprnglem12  21791  psgnghm  21879  mplcoe1  22339  mplcoe5  22342  evlseu  22385  mhpsclcl  22461  mdetunilem7  22926  mdetunilem9  22928  chcoeffeq  23197  cnindis  23603  lmss  23609  lmcls  23613  lmcnp  23615  hausnei  23639  cmpsub  23711  tgcmp  23712  fiuncmp  23715  cmpfi  23719  bwth  23721  1stcrest  23764  2ndcdisj  23768  1stccnp  23774  comppfsc  23844  1stckgenlem  23865  txcls  23916  txcn  23938  txlm  23960  tx1stc  23962  xkococn  23972  hmphdis  24108  ptcmpfi  24125  isfild  24170  fgss2  24186  filconn  24195  trfil2  24199  ufileu  24231  filufint  24232  elfm2  24260  flftg  24308  fclssscls  24330  fclscf  24337  ufilcmp  24344  cnpfcf  24353  alexsubb  24358  alexsubALTlem4  24362  alexsubALT  24363  qustgpopn  24432  tsmsxp  24467  isust  24516  xmettri2  24652  blin2  24741  setsmstopn  24790  met2ndc  24835  metcnp3  24852  tngtopn  24962  reconnlem2  25140  xrge0tsms  25147  fsumcn  25184  bndth  25272  iscmet3lem2  25606  iscmet3  25607  ivthlem1  25765  ivthlem2  25766  ivthlem3  25767  ovolfiniun  25815  volfiniun  25861  ioombl1lem4  25875  ismbf3d  25968  mbfi1flimlem  26036  itg2seq  26056  itgfsum  26140  ellimc3  26192  dvmptfsum  26288  c1liplem1  26309  plypf1  26524  plydivex  26611  aannenlem1  26648  ulmval  26700  ulmcau  26715  ulmbdd  26718  ulmcn  26719  ulmdvlem3  26722  sineq0  26845  efopn  26979  cxpeq  27078  logbgcd1irr  27115  rlimcnp  27286  xrlimcnp  27289  lgsdir2lem2  27646  lgsne0  27655  2lgsoddprm  27736  2sqlem6  27743  2sqlem10  27748  2sqreunnltblem  27771  ltsval2  28006  noetasuplem4  28086  conway  28158  madebdayim  28267  addsass  28384  oncutlt  28643  oniso  28650  addonbday  28658  n0ssoldg  28732  bdayn0p1  28748  oldfib  28756  bdaypw2n0bndlem  28842  bdayfinbndlem1  28846  z12bdaylem1  28849  z12zsodd  28861  axcontlem2  29536  uhgr0vb  29643  uvtx01vtx  29971  uvtxupgrres  29982  fusgrn0degnn0  30073  finsumvtxdg2size  30124  cusgrm1rusgr  30156  wlkv0  30223  wlklenvclwlk  30227  subgrwlk  30262  uspgrn2crct  30390  umgr2cycllem  30739  umgr2cycl  30740  frrusgrord  30935  numclwwlk1lem2fo  30952  isgrpo  31092  grpoidinvlem3  31101  vcdi  31160  vcdir  31161  vcass  31162  nvs  31258  nvtri  31265  blocnilem  31399  chintcli  31926  hsupss  31936  shlej1  31955  elspansn4  32168  spansncvi  32247  hoaddsub  32411  lnopl  32509  lnfnl  32526  riesz4i  32658  pjnormssi  32763  pj3si  32802  stlei  32835  stcltr2i  32870  dmdmd  32895  dmdbr5  32903  mdslmd1lem2  32921  atssma  32973  atcvatlem  32980  chirredlem1  32985  atcvat4i  32992  mdsymlem2  32999  mdsymlem6  33003  sumdmdlem2  33014  cdjreui  33027  elimifd  33132  disjxpin  33175  xrge0infss  33345  expgt0b  33401  xrge0tsmsd  33627  gsumvsca1  33780  gsumvsca2  33781  lmxrge0  34577  ismeas  34825  eulerpartlemb  34993  bnj849  35548  bnj1110  35605  axprALT2  35723  trssfir1om  35726  fineqvinfep  35776  trssfir1omregs  35787  cusgredgex2  35886  cusgr3cyclex  35890  connpconn  35979  cvmseu  36020  cvmliftlem15  36042  cvmlift2lem1  36046  cvmlift2lem12  36058  satfv0fun  36115  satffunlem  36145  mclsind  36314  r1peuqusdeg1  36387  dfon2lem3  36527  dfon2lem4  36528  dfon2lem6  36530  dfon2lem8  36532  dfon2lem9  36533  hbntg  36547  cgrdegen  36749  funtransport  36776  ifscgr  36789  cgrxfr  36800  brofs2  36822  brifs2  36823  idinside  36829  btwnconn1lem7  36838  btwnconn1lem11  36842  btwnconn1lem12  36843  btwnconn1lem14  36845  broutsideof2  36867  btwnoutside  36870  outsideoftr  36874  nmulprop  36919  in-ax8  36993  ss-ax8  36994  finminlem  37086  ntruni  37095  neibastop1  37127  ontgval  37199  ordtop  37204  ordcmp  37215  onint1  37217  bj-alrimdh  37474  bj-spimnfe  37503  bj-spimenfa  37504  bj-cbveximd  37511  bj-spvew  37515  bj-cbvexvv  37519  bj-ax12w  37557  axc11n11r  37565  bj-ax12v3  37567  bj-nnfan  37636  bj-nnfand  37637  bj-19.42t  37647  bj-sbft  37660  bj-nnflemea  37671  bj-hbaeb2  37710  bj-spcimdv  37787  bj-spcimdvv  37788  bj-sngltag  37876  bj-xtagex  37882  bj-axseprep  37970  bj-0int  38002  bj-ismooredr  38010  bj-inftyexpiinj  38110  nlpfvineqsn  38312  wl-ax13lem1  38397  wl-speqv  38434  wl-sbcom2d  38473  tan2h  38515  ptrest  38517  poimirlem20  38538  poimirlem22  38540  poimirlem26  38544  poimirlem30  38548  poimirlem31  38549  poimirlem32  38550  heicant  38553  voliunnfl  38562  volsupnfl  38563  itg2addnclem2  38570  itg2addnc  38572  itg2gt0cn  38573  ftc2nc  38600  filbcmb  38654  sdclem2  38656  seqpo  38661  nninfnub  38665  neificl  38667  prdstotbnd  38708  cnpwstotbnd  38711  heibor1lem  38723  heibor  38735  bfplem2  38737  opidonOLD  38766  exidu1  38770  grpokerinj  38807  rngoideu  38817  rngodi  38818  rngodir  38819  rngmgmbs4  38845  divrngidl  38942  prnc  38981  rsp3eq  39279  eqvrelqsel  39612  erimeq2  39675  prter2  39918  ax4fromc4  39931  hbae-o  39940  dvelimf-o  39966  ax12indn  39980  ax12inda2  39984  ax12a2-o  39987  l1cvpat  40091  atcvrj0  40465  pmaple  40798  paddasslem5  40861  pclfinN  40937  osumcllem11N  41003  pexmidlem8N  41014  dvheveccl  42149  dihord6apre  42293  lpolconN  42524  lcmineqlem1  43059  oexpreposd  43359  sn-it0e0  43447  cnreeu  43534  eu6w  43667  isnacs3  43700  pellexlem5  43819  pellex  43821  jm2.18  43974  jm2.15nn0  43989  jm2.16nn0  43990  dford3lem2  44013  ttac  44022  onexomgt  44227  onexoegt  44230  omabs2  44318  omcl3g  44320  tfsconcat0b  44332  naddgeoa  44380  safesnsupfiss  44400  rp-isfinite5  44502  cnvssb  44571  clcnvlem  44608  iunrelexpuztr  44704  rfovcnvf1od  44989  ntrrn  45107  nzss  45286  pm11.71  45366  axc11next  45375  hbntal  45521  eel2122old  45685  relwf  45935  modelaxreplem1  45946  ssclaxsep  45950  wfac8prim  45970  hfrel  45998  fsetsnf1  48091  2reu8i  48152  afvelima  48206  rlimdmafv  48216  rlimdmafv2  48297  elsprel  48526  sfprmdvdsmersenne  48657  perfectALTVlem2  48789  fpprwppr  48806  uhgrimedgi  48957  isuspgrim0lem  48960  uhgrimisgrgric  48998  gpgcubic  49146  gpg5nbgr3star  49148  pgnioedg1  49175  pgnioedg2  49176  pgnioedg3  49177  pgnioedg4  49178  pgnioedg5  49179  copisnmnd  49235  funcringcsetcALTV2lem8  49363  funcringcsetclem8ALTV  49386  lindslinindsimp2lem5  49543  nn0sumshdig  49704  prelrrx2b  49795  itscnhlc0yqe  49840  iscnrm3lem2  50012  diag1f1lem  50383  spd  50755  aacllem  50908