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  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  3622  moeq3  3670  reuimrmo  3703  sbeqalb  3801  srcmpltd  4432  replem  5243  csbexg  5267  ralxfrd  5373  ralxfrd2  5377  ralxfrALT  5380  copsexgwOLD  5467  copsexg  5468  pwssun  5547  somo  5602  ssrel  5763  relssres  6015  dmsnopg  6209  dfco2a  6242  dfpo2  6294  frpoinsg  6341  tz7.7  6383  ordunidif  6408  suctr  6446  trsucss  6448  suc11  6467  imadif  6617  dffv2  6973  fvmptd3f  7002  fvmptnf  7009  foco2  7102  fconst5  7205  fvf1pr  7308  isores3  7336  riotaxfrd  7404  ovmpt4g  7560  ovmpos  7561  ov2gf  7562  ovmpodf  7569  sorpsscmpl  7735  abnexg  7755  onint  7789  limuni3  7848  tfisg  7850  tfis  7851  tfinds  7856  limomss  7867  peano5  7890  fo2ndf  8118  frxp  8124  xpord2pred  8143  xpord2indlem  8145  soseq  8157  suppss2  8198  suppssfv  8200  rntpos  8237  fprlem1  8299  fprresex  8309  wfr3g  8318  onfununi  8330  smofvon2  8345  smo11  8353  smoord  8354  tfrlem11  8377  tz7.44-2  8396  tz7.48lem  8430  tz7.48-1  8432  tz7.49  8434  tz7.49c  8435  omordi  8553  omord  8555  omass  8567  oneo  8568  omeulem1  8569  omopth2  8571  oewordri  8580  oeworde  8581  nnmordi  8619  nnmord  8620  omabs  8639  nnneo  8643  omsmo  8646  naddcllem  8664  qsel  8796  eceqoveq  8822  domunsncan  9075  sbthlem1  9085  2pwuninel  9130  mapen  9139  infensuc  9153  rexdif1en  9155  findcard2  9159  pssnn  9163  ssfi  9167  sucdom2  9197  php  9201  onomeneq  9208  0sdom1dom  9216  sdom1  9220  dif1ennnALT  9247  ac6sfi  9254  frfi  9255  unblem1  9262  unblem2  9263  unbnn2  9267  domunfican  9291  fodomfir  9297  ixpfi2  9317  finsschain  9326  unifi3  9329  marypha1lem  9403  oiexg  9507  brwdom3  9554  inf3lem2  9608  inf3lem3  9609  cantnfval2  9648  cantnflt  9651  cantnflem1  9668  cnfcom  9679  ttrclss  9699  trcl  9707  epfrs  9710  frmin  9731  frinsg  9733  frr3g  9738  frrlem15  9739  r1sdom  9756  cardsdomel  9979  carduni  9986  infpwfien  10065  carduniima  10099  dfac5  10131  dfac12r  10149  dfac12k  10150  kmlem11  10163  djuinf  10191  infxp  10216  cfsuc  10259  cfcoflem  10274  coftr  10275  infpssr  10310  fin23lem30  10344  isf32lem1  10355  isf34lem6  10382  fin1a2lem13  10414  fin1a2s  10416  axcc2lem  10438  domtriomlem  10444  axcclem  10459  ac6num  10481  zorn2lem5  10502  zorn2lem6  10503  axdclem2  10522  alephval2  10581  alephreg  10591  pwcfsdom  10592  axregndlem1  10611  axregnd  10613  axacndlem1  10616  axacndlem2  10617  axacndlem3  10618  axacndlem4  10619  axacnd  10621  gchi  10633  fpwwe2lem12  10651  canthp1  10663  gchpwdom  10679  wunfi  10730  tskwe2  10782  inar1  10784  gruen  10821  intgru  10823  indpi  10916  nqereu  10938  ltbtwnnq  10987  prnmadd  11006  genpcd  11015  prlem934  11042  ltexprlem1  11045  ltexprlem2  11046  ltexprlem7  11051  ltaprlem  11053  ltapr  11054  reclem4pr  11059  suplem2pr  11062  mulcmpblnr  11080  recexsrlem  11112  mulgt0sr  11114  supsrlem  11120  axpre-sup  11178  1re  11232  dedekindle  11398  addlsub  11654  recex  11870  nnunb  12524  0mnnnnn0  12560  prime  12702  zeo  12707  fnn0ind  12720  zindd  12722  btwnz  12724  lbzbi  12985  xrub  13364  elfznelfzo  13829  fvf1tp  13850  addmodlteq  14010  facwordi  14353  fiinfnf1o  14414  hashclb  14422  hashdom  14443  hashf1lem2  14521  seqcoll  14529  brfi1indALT  14575  ccatalpha  14660  pfxccatin12lem2a  14796  swrdrevpfx  14838  limsupbnd2  15570  rlimdm  15638  o1of2  15700  rlimno1  15741  isercoll  15755  caurcvg2  15765  caucvgb  15767  serf0  15768  zsum  15804  fsum2dlem  15856  fsum2d  15857  fsumabs  15888  fsumrlim  15898  fsumo1  15899  fsumiun  15908  zprod  16024  fprod2dlem  16067  fprod2d  16068  odd2np1  16431  ndvdssub  16499  dfgcd2  16636  nprm  16778  maxprmfct  16800  rpexp  16813  pc2dvds  16971  pcfac  16991  unbenlem  17000  4sqlem12  17048  4sqlem17  17053  vdwlem13  17085  prmlem0  17197  mreiincl  17680  sscfn1  17906  initoid  18090  termoid  18091  funcestrcsetclem8  18235  funcsetcestrclem8  18250  pospo  18431  cnvpsb  18667  dirtr  18690  mgmidpfod  18770  mulgaddcom  19221  mulginvcom  19222  gaass  19424  cntz2ss  19462  elsymgbas  19501  symgfix2  19543  pmtrfrn  19585  psgnran  19642  odmulg  19683  odhash3  19703  sylow2alem1  19744  sylow2alem2  19745  pj1eu  19823  efgs1b  19863  efgsfo  19866  efgredlemc  19872  efgredeu  19879  frgpuptinv  19898  lt6abl  20022  ghmcyg  20023  ablfac1eulem  20201  pgpfac1lem5  20208  ablsimpgfindlem1  20236  gsumle  20272  ringinvnz1ne0  20442  irredmul  20570  rnghmsscmap2  20791  rnghmsscmap  20792  rhmsscmap2  20820  rhmsscmap  20821  acsfn1p  20965  lspextmo  21240  lspsncv0  21333  pzriprnglem12  21705  psgnghm  21793  mplcoe1  22253  mplcoe5  22256  evlseu  22299  mhpsclcl  22375  mdetunilem7  22840  mdetunilem9  22842  chcoeffeq  23111  cnindis  23517  lmss  23523  lmcls  23527  lmcnp  23529  hausnei  23553  cmpsub  23625  tgcmp  23626  fiuncmp  23629  cmpfi  23633  bwth  23635  1stcrest  23678  2ndcdisj  23682  1stccnp  23688  comppfsc  23758  1stckgenlem  23779  txcls  23830  txcn  23852  txlm  23874  tx1stc  23876  xkococn  23886  hmphdis  24022  ptcmpfi  24039  isfild  24084  fgss2  24100  filconn  24109  trfil2  24113  ufileu  24145  filufint  24146  elfm2  24174  flftg  24222  fclssscls  24244  fclscf  24251  ufilcmp  24258  cnpfcf  24267  alexsubb  24272  alexsubALTlem4  24276  alexsubALT  24277  qustgpopn  24346  tsmsxp  24381  isust  24430  xmettri2  24566  blin2  24655  setsmstopn  24704  met2ndc  24749  metcnp3  24766  tngtopn  24876  reconnlem2  25054  xrge0tsms  25061  fsumcn  25098  bndth  25186  iscmet3lem2  25520  iscmet3  25521  ivthlem1  25679  ivthlem2  25680  ivthlem3  25681  ovolfiniun  25729  volfiniun  25775  ioombl1lem4  25789  ismbf3d  25882  mbfi1flimlem  25950  itg2seq  25970  itgfsum  26054  ellimc3  26106  dvmptfsum  26202  c1liplem1  26223  plypf1  26438  plydivex  26527  aannenlem1  26564  ulmval  26616  ulmcau  26631  ulmbdd  26634  ulmcn  26635  ulmdvlem3  26638  sineq0  26761  efopn  26895  cxpeq  26994  logbgcd1irr  27031  rlimcnp  27202  xrlimcnp  27205  lgsdir2lem2  27562  lgsne0  27571  2lgsoddprm  27652  2sqlem6  27659  2sqlem10  27664  2sqreunnltblem  27687  ltsval2  27892  noetasuplem4  27972  conway  28044  madebdayim  28153  addsass  28270  oncutlt  28529  oniso  28536  addonbday  28544  n0ssoldg  28618  bdayn0p1  28634  oldfib  28642  bdaypw2n0bndlem  28728  bdayfinbndlem1  28732  z12bdaylem1  28735  z12zsodd  28747  axcontlem2  29422  uhgr0vb  29529  uvtx01vtx  29857  uvtxupgrres  29868  fusgrn0degnn0  29959  finsumvtxdg2size  30010  cusgrm1rusgr  30042  wlkv0  30109  wlklenvclwlk  30113  subgrwlk  30148  uspgrn2crct  30276  umgr2cycllem  30625  umgr2cycl  30626  frrusgrord  30821  numclwwlk1lem2fo  30838  isgrpo  30978  grpoidinvlem3  30987  vcdi  31046  vcdir  31047  vcass  31048  nvs  31144  nvtri  31151  blocnilem  31285  chintcli  31812  hsupss  31822  shlej1  31841  elspansn4  32054  spansncvi  32133  hoaddsub  32297  lnopl  32395  lnfnl  32412  riesz4i  32544  pjnormssi  32649  pj3si  32688  stlei  32721  stcltr2i  32756  dmdmd  32781  dmdbr5  32789  mdslmd1lem2  32807  atssma  32859  atcvatlem  32866  chirredlem1  32871  atcvat4i  32878  mdsymlem2  32885  mdsymlem6  32889  sumdmdlem2  32900  cdjreui  32913  elimifd  33018  disjxpin  33061  xrge0infss  33231  expgt0b  33287  xrge0tsmsd  33513  gsumvsca1  33666  gsumvsca2  33667  lmxrge0  34462  ismeas  34710  eulerpartlemb  34879  bnj849  35434  bnj1110  35491  axprALT2  35617  trssfir1om  35621  fineqvinfep  35651  trssfir1omregs  35662  cusgredgex2  35721  cusgr3cyclex  35725  connpconn  35814  cvmseu  35855  cvmliftlem15  35877  cvmlift2lem1  35881  cvmlift2lem12  35893  satfv0fun  35950  satffunlem  35980  mclsind  36149  r1peuqusdeg1  36222  dfon2lem3  36362  dfon2lem4  36363  dfon2lem6  36365  dfon2lem8  36367  dfon2lem9  36368  hbntg  36382  cgrdegen  36584  funtransport  36611  ifscgr  36624  cgrxfr  36635  brofs2  36657  brifs2  36658  idinside  36664  btwnconn1lem7  36673  btwnconn1lem11  36677  btwnconn1lem12  36678  btwnconn1lem14  36680  broutsideof2  36702  btwnoutside  36705  outsideoftr  36709  nmulprop  36770  in-ax8  36844  ss-ax8  36845  finminlem  36937  ntruni  36946  neibastop1  36978  ontgval  37050  ordtop  37055  ordcmp  37066  onint1  37068  bj-alrimdh  37325  bj-spimnfe  37354  bj-spimenfa  37355  bj-cbveximd  37362  bj-spvew  37366  bj-cbvexvv  37370  bj-ax12w  37408  axc11n11r  37416  bj-ax12v3  37418  bj-nnfan  37487  bj-nnfand  37488  bj-19.42t  37498  bj-sbft  37511  bj-nnflemea  37522  bj-hbaeb2  37561  bj-spcimdv  37638  bj-spcimdvv  37639  bj-sngltag  37727  bj-xtagex  37733  bj-axseprep  37819  bj-0int  37851  bj-ismooredr  37859  bj-inftyexpiinj  37961  nlpfvineqsn  38163  wl-ax13lem1  38248  wl-speqv  38285  wl-sbcom2d  38324  tan2h  38366  ptrest  38368  poimirlem20  38389  poimirlem22  38391  poimirlem26  38395  poimirlem30  38399  poimirlem31  38400  poimirlem32  38401  heicant  38404  voliunnfl  38413  volsupnfl  38414  itg2addnclem2  38421  itg2addnc  38423  itg2gt0cn  38424  ftc2nc  38451  filbcmb  38490  sdclem2  38492  seqpo  38497  nninfnub  38501  neificl  38503  prdstotbnd  38544  cnpwstotbnd  38547  heibor1lem  38559  heibor  38571  bfplem2  38573  opidonOLD  38602  exidu1  38606  grpokerinj  38643  rngoideu  38653  rngodi  38654  rngodir  38655  rngmgmbs4  38681  divrngidl  38778  prnc  38817  rsp3eq  39115  eqvrelqsel  39448  erimeq2  39511  prter2  39754  ax4fromc4  39767  hbae-o  39776  dvelimf-o  39802  ax12indn  39816  ax12inda2  39820  ax12a2-o  39823  l1cvpat  39927  atcvrj0  40301  pmaple  40634  paddasslem5  40697  pclfinN  40773  osumcllem11N  40839  pexmidlem8N  40850  dvheveccl  41985  dihord6apre  42129  lpolconN  42360  lcmineqlem1  42895  oexpreposd  43197  sn-it0e0  43291  cnreeu  43378  eu6w  43522  isnacs3  43555  pellexlem5  43674  pellex  43676  jm2.18  43829  jm2.15nn0  43844  jm2.16nn0  43845  dford3lem2  43868  ttac  43877  onexomgt  44082  onexoegt  44085  omabs2  44173  omcl3g  44175  tfsconcat0b  44187  naddgeoa  44235  safesnsupfiss  44255  rp-isfinite5  44357  cnvssb  44426  clcnvlem  44463  iunrelexpuztr  44559  rfovcnvf1od  44844  ntrrn  44962  nzss  45141  pm11.71  45221  axc11next  45230  hbntal  45376  eel2122old  45540  relwf  45790  modelaxreplem1  45801  ssclaxsep  45805  wfac8prim  45825  fsetsnf1  47940  2reu8i  48001  afvelima  48055  rlimdmafv  48065  rlimdmafv2  48146  elsprel  48375  sfprmdvdsmersenne  48506  perfectALTVlem2  48638  fpprwppr  48655  uhgrimedgi  48806  isuspgrim0lem  48809  uhgrimisgrgric  48847  gpgcubic  48995  gpg5nbgr3star  48997  pgnioedg1  49024  pgnioedg2  49025  pgnioedg3  49026  pgnioedg4  49027  pgnioedg5  49028  copisnmnd  49084  funcringcsetcALTV2lem8  49212  funcringcsetclem8ALTV  49235  lindslinindsimp2lem5  49392  nn0sumshdig  49553  prelrrx2b  49644  itscnhlc0yqe  49689  iscnrm3lem2  49861  diag1f1lem  50232  spd  50604  setrec1lem4  50616  setrec2fun  50618  aacllem  50772