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  1895  stdpc5v  1970  19.37imv  1979  ax12w  2169  ax13dgen2  2174  ax12v  2213  spsd  2223  nf5r  2230  axc4  2351  equs5eALT  2396  ax13lem1  2403  nfeqf  2410  hbae  2460  ax12vALT  2498  2ax6elem  2499  sb1  2507  euimmo  2641  necon2ad  2970  necon4ad  2974  r19.37v  3188  rr19.28v  3621  moeq3  3669  reuimrmo  3702  sbeqalb  3800  srcmpltd  4431  replem  5240  csbexg  5263  ralxfrd  5369  ralxfrd2  5373  ralxfrALT  5376  copsexgwOLD  5460  copsexg  5461  pwssun  5542  somo  5597  ssrel  5758  relssres  6010  dfrn7  6065  cnvssb  6188  dmsnopg  6214  dfco2a  6247  dfpo2  6299  frpoinsg  6346  tz7.7  6388  ordunidif  6413  suctr  6451  trsucss  6453  suc11  6472  imadif  6624  dffv2  6980  fvmptd3f  7009  fvmptnf  7016  foco2  7109  fconst5  7212  fvf1pr  7315  isores3  7343  riotaxfrd  7411  ovmpt4g  7567  ovmpos  7568  ov2gf  7569  ovmpodf  7576  sorpsscmpl  7750  abnexg  7770  onint  7804  limuni3  7863  tfisg  7865  tfis  7866  tfinds  7871  limomss  7882  peano5  7905  fo2ndf  8132  frxp  8138  xpord2pred  8162  xpord2indlem  8164  soseq  8176  suppss2  8217  suppssfv  8219  rntpos  8256  fprlem1  8318  fprresex  8328  wfr3g  8337  onfununi  8349  smofvon2  8364  smo11  8372  smoord  8373  tfrlem11  8396  tz7.44-2  8415  tz7.48lemOLD  8451  tz7.48-1  8453  tz7.49  8455  tz7.49c  8456  omordi  8574  omord  8576  omass  8588  oneo  8589  omeulem1  8590  omopth2  8592  oewordri  8601  oeworde  8602  nnmordi  8640  nnmord  8641  omabs  8660  nnneo  8664  omsmo  8667  naddcllem  8685  qsel  8817  eceqoveq  8843  domunsncan  9096  sbthlem1  9106  2pwuninel  9151  mapen  9160  infensuc  9174  rexdif1en  9176  findcard2  9180  pssnn  9184  ssfi  9188  sucdom2  9218  php  9222  onomeneq  9229  0sdom1dom  9237  sdom1  9241  dif1ennnALT  9268  ac6sfi  9275  frfi  9276  unblem1  9284  unblem2  9285  unbnn2  9289  domunfican  9313  fodomfir  9319  ixpfi2  9339  finsschain  9348  unifi3  9351  marypha1lem  9425  oiexg  9529  brwdom3  9576  inf3lem2  9630  inf3lem3  9631  cantnfval2  9670  cantnflt  9673  cantnflem1  9690  cnfcom  9701  ttrclss  9721  trcl  9729  epfrs  9732  frmin  9753  frinsg  9755  frr3g  9760  frrlem15  9761  r1sdom  9781  setrec1lem4  9971  setrec2fun  9973  cardsdomel  10055  carduni  10062  infpwfien  10141  carduniima  10175  dfac5  10207  dfac12r  10225  dfac12k  10226  kmlem11  10239  djuinf  10267  infxp  10292  cfsuc  10335  cfcoflem  10350  coftr  10351  infpssr  10386  fin23lem30  10420  isf32lem1  10431  isf34lem6  10458  fin1a2lem13  10490  fin1a2s  10492  axcc2lem  10514  domtriomlem  10520  axcclem  10535  ac6num  10557  zorn2lem5  10578  zorn2lem6  10579  axdclem2  10598  alephval2  10657  alephreg  10667  pwcfsdom  10668  axregndlem1  10687  axregnd  10689  axacndlem1  10692  axacndlem2  10693  axacndlem3  10694  axacndlem4  10695  axacnd  10697  gchi  10709  fpwwe2lem12  10727  canthp1  10739  gchpwdom  10755  wunfi  10806  tskwe2  10858  inar1  10860  gruen  10897  intgru  10899  indpi  10992  nqereu  11014  ltbtwnnq  11063  prnmadd  11082  genpcd  11091  prlem934  11118  ltexprlem1  11121  ltexprlem2  11122  ltexprlem7  11127  ltaprlem  11129  ltapr  11130  reclem4pr  11135  suplem2pr  11138  mulcmpblnr  11156  recexsrlem  11188  mulgt0sr  11190  supsrlem  11196  axpre-sup  11254  1re  11308  dedekindle  11474  addlsub  11732  recex  11948  nnunb  12602  0mnnnnn0  12638  prime  12780  zeo  12785  fnn0ind  12798  zindd  12800  btwnz  12802  lbzbi  13063  xrub  13442  elfznelfzo  13908  fvf1tp  13929  addmodlteq  14089  facwordi  14433  fiinfnf1o  14494  hashclb  14502  hashdom  14523  hashf1lem2  14601  seqcoll  14609  brfi1indALT  14655  ccatalpha  14740  pfxccatin12lem2a  14876  swrdrevpfx  14918  limsupbnd2  15650  rlimdm  15718  o1of2  15780  rlimno1  15821  isercoll  15835  caurcvg2  15845  caucvgb  15847  serf0  15848  zsum  15884  fsum2dlem  15936  fsum2d  15937  fsumabs  15968  fsumrlim  15978  fsumo1  15979  fsumiun  15988  zprod  16104  fprod2dlem  16147  fprod2d  16148  odd2np1  16511  ndvdssub  16579  dfgcd2  16719  nprm  16863  maxprmfct  16885  rpexp  16898  pc2dvds  17057  pcfac  17077  unbenlem  17086  4sqlem12  17134  4sqlem17  17139  vdwlem13  17171  prmlem0  17283  mreiincl  17766  sscfn1  17992  initoid  18176  termoid  18177  funcestrcsetclem8  18321  funcsetcestrclem8  18336  pospo  18517  cnvpsb  18753  dirtr  18776  mgmidpfod  18857  mulgaddcom  19308  mulginvcom  19309  gaass  19511  cntz2ss  19549  elsymgbas  19588  symgfix2  19630  pmtrfrn  19672  psgnran  19729  odmulg  19770  odhash3  19790  sylow2alem1  19831  sylow2alem2  19832  pj1eu  19910  efgs1b  19950  efgsfo  19953  efgredlemc  19959  efgredeu  19966  frgpuptinv  19985  lt6abl  20109  ghmcyg  20110  ablfac1eulem  20288  pgpfac1lem5  20295  ablsimpgfindlem1  20323  gsumle  20359  ringinvnz1ne0  20531  irredmul  20659  rnghmsscmap2  20881  rnghmsscmap  20882  rhmsscmap2  20910  rhmsscmap  20911  acsfn1p  21056  lspextmo  21331  lspsncv0  21424  pzriprnglem12  21798  psgnghm  21886  mplcoe1  22346  mplcoe5  22349  evlseu  22392  mhpsclcl  22468  mdetunilem7  22933  mdetunilem9  22935  chcoeffeq  23204  cnindis  23610  lmss  23616  lmcls  23620  lmcnp  23622  hausnei  23646  cmpsub  23718  tgcmp  23719  fiuncmp  23722  cmpfi  23726  bwth  23728  1stcrest  23771  2ndcdisj  23775  1stccnp  23781  comppfsc  23851  1stckgenlem  23872  txcls  23923  txcn  23945  txlm  23967  tx1stc  23969  xkococn  23979  hmphdis  24115  ptcmpfi  24132  isfild  24177  fgss2  24193  filconn  24202  trfil2  24206  ufileu  24238  filufint  24239  elfm2  24267  flftg  24315  fclssscls  24337  fclscf  24344  ufilcmp  24351  cnpfcf  24360  alexsubb  24365  alexsubALTlem4  24369  alexsubALT  24370  qustgpopn  24439  tsmsxp  24474  isust  24523  xmettri2  24659  blin2  24748  setsmstopn  24797  met2ndc  24842  metcnp3  24859  tngtopn  24969  reconnlem2  25147  xrge0tsms  25154  fsumcn  25191  bndth  25279  iscmet3lem2  25613  iscmet3  25614  ivthlem1  25772  ivthlem2  25773  ivthlem3  25774  ovolfiniun  25822  volfiniun  25868  ioombl1lem4  25882  ismbf3d  25975  mbfi1flimlem  26043  itg2seq  26063  itgfsum  26147  ellimc3  26199  dvmptfsum  26295  c1liplem1  26316  plypf1  26531  plydivex  26618  aannenlem1  26655  ulmval  26707  ulmcau  26722  ulmbdd  26725  ulmcn  26726  ulmdvlem3  26729  sineq0  26852  efopn  26986  cxpeq  27085  logbgcd1irr  27122  rlimcnp  27293  xrlimcnp  27296  lgsdir2lem2  27653  lgsne0  27662  2lgsoddprm  27743  2sqlem6  27750  2sqlem10  27755  2sqreunnltblem  27778  ltsval2  28013  noetasuplem4  28093  conway  28165  madebdayim  28274  addsass  28391  oncutlt  28650  oniso  28657  addonbday  28665  n0ssoldg  28739  bdayn0p1  28755  oldfib  28763  bdaypw2n0bndlem  28849  bdayfinbndlem1  28853  z12bdaylem1  28856  z12zsodd  28868  axcontlem2  29543  uhgr0vb  29650  uvtx01vtx  29978  uvtxupgrres  29989  fusgrn0degnn0  30080  finsumvtxdg2size  30131  cusgrm1rusgr  30163  wlkv0  30230  wlklenvclwlk  30234  subgrwlk  30269  uspgrn2crct  30397  umgr2cycllem  30746  umgr2cycl  30747  frrusgrord  30942  numclwwlk1lem2fo  30959  isgrpo  31099  grpoidinvlem3  31108  vcdi  31167  vcdir  31168  vcass  31169  nvs  31265  nvtri  31272  blocnilem  31406  chintcli  31933  hsupss  31943  shlej1  31962  elspansn4  32175  spansncvi  32254  hoaddsub  32418  lnopl  32516  lnfnl  32533  riesz4i  32665  pjnormssi  32770  pj3si  32809  stlei  32842  stcltr2i  32877  dmdmd  32902  dmdbr5  32910  mdslmd1lem2  32928  atssma  32980  atcvatlem  32987  chirredlem1  32992  atcvat4i  32999  mdsymlem2  33006  mdsymlem6  33010  sumdmdlem2  33021  cdjreui  33034  elimifd  33139  disjxpin  33182  xrge0infss  33352  expgt0b  33408  xrge0tsmsd  33634  gsumvsca1  33787  gsumvsca2  33788  lmxrge0  34584  ismeas  34832  eulerpartlemb  35000  bnj849  35555  bnj1110  35612  soinfdom  35717  axprALT2  35734  trssfir1om  35737  acwer1prclem  35759  fineqvinfep  35793  trssfir1omregs  35804  onprcf1acwevdlem1  35895  cusgredgex2  35907  cusgr3cyclex  35911  connpconn  36000  cvmseu  36041  cvmliftlem15  36063  cvmlift2lem1  36067  cvmlift2lem12  36079  satfv0fun  36136  satffunlem  36166  mclsind  36335  r1peuqusdeg1  36408  dfon2lem3  36547  dfon2lem4  36548  dfon2lem6  36550  dfon2lem8  36552  dfon2lem9  36553  hbntg  36567  cgrdegen  36769  funtransport  36796  ifscgr  36809  cgrxfr  36820  brofs2  36842  brifs2  36843  idinside  36849  btwnconn1lem7  36858  btwnconn1lem11  36862  btwnconn1lem12  36863  btwnconn1lem14  36865  broutsideof2  36887  btwnoutside  36890  outsideoftr  36894  nmulprop  36939  in-ax8  37013  ss-ax8  37014  finminlem  37106  ntruni  37115  neibastop1  37147  ontgval  37219  ordtop  37224  ordcmp  37235  onint1  37237  bj-alrimdh  37494  bj-spimnfe  37523  bj-spimenfa  37524  bj-cbveximd  37531  bj-spvew  37535  bj-cbvexvv  37539  bj-ax12w  37577  axc11n11r  37585  bj-ax12v3  37587  bj-nnfan  37656  bj-nnfand  37657  bj-19.42t  37667  bj-sbft  37680  bj-nnflemea  37691  bj-hbaeb2  37730  bj-spcimdv  37807  bj-spcimdvv  37808  bj-sngltag  37896  bj-xtagex  37902  bj-axseprep  37990  bj-0int  38022  bj-ismooredr  38030  bj-inftyexpiinj  38131  nlpfvineqsn  38333  wl-ax13lem1  38418  wl-speqv  38455  wl-sbcom2d  38494  tan2h  38536  ptrest  38538  poimirlem20  38559  poimirlem22  38561  poimirlem26  38565  poimirlem30  38569  poimirlem31  38570  poimirlem32  38571  heicant  38574  voliunnfl  38583  volsupnfl  38584  itg2addnclem2  38591  itg2addnc  38593  itg2gt0cn  38594  ftc2nc  38621  filbcmb  38675  sdclem2  38677  seqpo  38682  nninfnub  38686  neificl  38688  prdstotbnd  38729  cnpwstotbnd  38732  heibor1lem  38744  heibor  38756  bfplem2  38758  opidonOLD  38787  exidu1  38791  grpokerinj  38828  rngoideu  38838  rngodi  38839  rngodir  38840  rngmgmbs4  38866  divrngidl  38963  prnc  39002  rsp3eq  39300  eqvrelqsel  39633  erimeq2  39696  prter2  39939  ax4fromc4  39952  hbae-o  39961  dvelimf-o  39987  ax12indn  40001  ax12inda2  40005  ax12a2-o  40008  l1cvpat  40112  atcvrj0  40486  pmaple  40819  paddasslem5  40882  pclfinN  40958  osumcllem11N  41024  pexmidlem8N  41035  dvheveccl  42170  dihord6apre  42314  lpolconN  42545  lcmineqlem1  43080  oexpreposd  43380  sn-it0e0  43468  cnreeu  43555  eu6w  43688  isnacs3  43721  pellexlem5  43840  pellex  43842  jm2.18  43995  jm2.15nn0  44010  jm2.16nn0  44011  dford3lem2  44034  ttac  44043  onexomgt  44243  onexoegt  44246  omabs2  44334  omcl3g  44336  tfsconcat0b  44348  naddgeoa  44396  safesnsupfiss  44416  rp-isfinite5  44518  clcnvlem  44623  iunrelexpuztr  44719  rfovcnvf1od  45004  ntrrn  45122  nzss  45301  pm11.71  45381  axc11next  45390  hbntal  45536  eel2122old  45700  cocanss2  45922  relwf  45957  modelaxreplem1  45968  ssclaxsep  45972  wfac8prim  45992  hfrel  46020  fsetsnf1  48122  2reu8i  48183  afvelima  48237  rlimdmafv  48247  rlimdmafv2  48328  elsprel  48557  sfprmdvdsmersenne  48688  perfectALTVlem2  48820  fpprwppr  48837  uhgrimedgi  48988  isuspgrim0lem  48991  uhgrimisgrgric  49029  gpgcubic  49177  gpg5nbgr3star  49179  pgnioedg1  49206  pgnioedg2  49207  pgnioedg3  49208  pgnioedg4  49209  pgnioedg5  49210  copisnmnd  49266  funcringcsetcALTV2lem8  49394  funcringcsetclem8ALTV  49417  lindslinindsimp2lem5  49574  nn0sumshdig  49735  prelrrx2b  49826  itscnhlc0yqe  49871  iscnrm3lem2  50043  diag1f1lem  50414  spd  50786  aacllem  50939