Theorem sylibr 134

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylibr.1	⊢ (𝜑 → 𝜓)
sylibr.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
sylibr	⊢ (𝜑 → 𝜒)

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylibr.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	biimpri 133	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbbr  136  pm5.74rd  183  bitri  184  3imtr4i  201  sylanbrc  417  mpnanrd  700  oibabs  722  dcim  849  dcstab  852  stdcndc  853  stdcndcOLD  854  dcand  941  dcor  944  dfifp2dc  990  3mix1  1193  3mix2  1194  3jca  1204  syl3anbrc  1208  syl21anbrc  1209  inegd  1417  pclem6  1419  xoranor  1422  dcfrompeirce  1495  nfxfrd  1524  nfd  1572  hban  1596  nfan1  1613  nford  1616  nfand  1617  hbim1  1619  nfal  1625  alexim  1694  nnal  1698  hbn  1699  nf4r  1719  19.34  1732  nfexd  1810  sbcof2  1859  nfsb2or  1886  sbidm  1900  nfdv  1926  nfd2  2078  nfeudv  2097  mon  2111  eumo  2114  mo23  2124  eu2  2127  eu3h  2128  exmodc  2133  exmonim  2134  mo2r  2135  mo3h  2136  bm1.1  2219  eqrdv  2232  3eltr4g  2320  abbi2dv  2355  abbi1dv  2356  nfcd  2381  nfcxfrd  2384  dcned  2420  neqned  2421  3netr4g  2449  necon3bi  2464  necon2ai  2468  nnral  2534  alral  2589  rspe  2593  rsp2e  2595  rgen2a  2598  ralrimi  2615  r19.27v  2672  r19.28v  2673  r19.27av  2680  r19.32r  2691  nfreudxy  2719  mormo  2763  nrexrmo  2768  cgsex2g  2852  cgsex4g  2853  spc2egv  2909  spc2gv  2910  spc3egv  2911  spc3gv  2912  rspce  2918  ceqex  2947  elrab3t  2975  elrabd  2978  mosubt  2997  mo2icl  2999  reu3  3010  reu6i  3011  2rmorex  3026  sbc5  3069  rspesbca  3131  rmo2ilem  3136  sbnfc2  3202  ssrd  3247  ssrdv  3248  3sstr4g  3285  eqsstrid  3288  ss2abdv  3315  abssdv  3316  rabssdv  3322  ss2rabdv  3323  ssun1  3386  unssad  3400  unssbd  3401  ssddif  3459  uneqin  3476  indifdir  3481  undif3ss  3486  reuss2  3505  n0rf  3525  reximdva0m  3528  rabxmdc  3544  ssindif0im  3572  minel  3574  ralidm  3614  ralm  3617  dcun  3623  ifmdc  3669  ifeqeqxdc  3673  disjsn2  3757  rabsnif  3763  absneu  3768  rabsneu  3769  opprc  3909  elunii  3924  dfnfc2  3937  uniss2  3950  unidif  3951  ssunieq  3952  intab  3983  iunss2  4041  iunssd  4042  iunxdif2  4045  invdisj  4107  disjiun  4109  3brtr4g  4148  trin  4223  triun  4226  truni  4227  trint  4228  iinexgm  4271  class2seteq  4281  pwuni  4310  exmid1dc  4318  exmidn0m  4319  exmidsssn  4320  exmid0el  4322  exmidel  4323  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  mss  4347  copsex2t  4366  euotd  4376  pwunim  4412  ispod  4430  sotricim  4449  exse  4462  frind  4478  trssord  4506  suctr  4547  pwnex  4575  eusvnf  4579  eusvnfb  4580  eusv2nf  4582  rexxfrd  4589  ralxfr2d  4590  rexxfr2d  4591  rabxfrd  4595  reuhypd  4597  eldifpw  4603  iunpw  4606  ssorduni  4614  onsucb  4630  onsucelsucr  4635  sucunielr  4637  ontriexmidim  4649  ordtri2or2exmidlem  4653  onsucelsucexmid  4657  reg2exmidlema  4661  setindel  4665  elirr  4668  orddisj  4673  en2lp  4681  suc11g  4684  ordsuc  4690  nlimsucg  4693  ordtri2or2exmid  4698  ontri2orexmidim  4699  zfregfr  4701  wessep  4705  tfi  4709  peano5  4725  limom  4741  peano2b  4742  nndceq0  4745  nnpredcl  4750  0nelrel  4801  eqrelrdv  4851  xpsspw  4867  relint  4881  relop  4910  eqbrrdva  4930  ssrelrn  4952  opeldm  4964  reldmm  4980  elres  5079  relssres  5081  elrelimasn  5133  exse2  5141  issref  5150  trin2  5159  dminss  5182  imainss  5183  rnxpid  5202  dmsn0el  5237  dmmptg  5265  relrelss  5294  cnviinm  5309  iotanul  5333  sniota  5348  dffun5r  5369  funmo  5372  funco  5397  funun  5402  fununmo  5403  fununfun  5404  funprg  5411  funtpg  5412  funtp  5414  fntpg  5417  fununi  5429  funcnvuni  5430  imadiflem  5440  imainlem  5442  funimaexglem  5444  isarep2  5448  fnunsn  5470  2elresin  5474  fnimadisj  5484  dmmptd  5494  fco  5532  funssxp  5537  fssres  5545  feu  5554  fimacnvdisj  5556  fabexg  5559  f00  5564  f0rn0  5567  f1co  5590  fores  5605  foco  5606  f1ores  5634  foimacnv  5637  f1oun  5639  fun11iun  5640  f1oco  5642  fo00  5657  brprcneu  5668  fv3  5698  relelfvdm  5707  nfvres  5711  nfunsn  5712  funfvbrb  5796  respreima  5810  dff2  5826  dff3im  5827  dffo4  5830  fvmptelcdm  5835  ffvresb  5845  f1oresrab  5847  fmptco  5848  fsn  5854  fcof  5868  fpr  5871  ftpg  5873  fsnunf  5889  fsnunfv  5890  elabrex  5936  dff1o6  5955  foeqcnvco  5969  fliftel1  5973  isores1  5993  isoini2  5998  riotasbc  6028  acexmidlemph  6051  acexmidlemcase  6053  oprabidlem  6089  brabvv  6107  eloprabga  6148  fnoprabg  6162  caovimo  6256  oprabexd  6333  uchoice  6344  fo1stresm  6368  fo2ndresm  6369  unielxp  6381  1st2ndbr  6391  opabn1stprc  6402  fmpoco  6425  1stconst  6430  2ndconst  6431  poxp  6441  spc2ed  6442  disjxp1  6445  elmpom  6447  suppsnopdc  6463  reldmtpos  6497  tposfun  6504  dftpos4  6507  smores  6536  smores2  6538  tfrlem1  6552  tfr0dm  6566  tfrlemibxssdm  6571  tfrlemibex  6573  tfrlemiubacc  6574  tfrlemi14d  6577  tfrexlem  6578  tfri1d  6579  tfr1onlembxssdm  6587  tfr1onlembex  6589  tfr1onlemubacc  6590  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllembxssdm  6600  tfrcllembex  6602  tfrcllemubacc  6603  tfrcllemres  6606  tfri3  6611  rdgon  6630  frecabcl  6643  frecfcllem  6648  frecrdg  6652  2oconcl  6685  nnsucelsuc  6737  nntri3or  6739  nndceq  6745  nndcel  6746  dcdifsnid  6750  ecexr  6785  brdifun  6807  ecelqsdm  6852  iinerm  6854  eroveu  6873  erovlem  6874  ecopovtrn  6879  ecopovtrng  6882  th3qlem1  6884  pmsspw  6930  map0b  6934  mapsnd  6936  mapsn  6938  mapsncnv  6943  ixpf  6968  uniixp  6969  ixpexgg  6970  resixp  6981  f1oen3g  7006  ssdomg  7031  domtr  7038  snfig  7069  modom  7074  enpr2d  7077  dom1o  7082  xpf1o  7110  xpmapenlem  7115  php5dom  7130  fidceq  7137  nnfi  7140  fiunsnnn  7151  findcard  7158  findcard2  7159  findcard2s  7160  ac6sfi  7168  fidcen  7169  tridc  7170  fimax2gtri  7172  finexdc  7173  elssdc  7175  eqsndc  7176  exmidpw  7181  exmidpweq  7182  exmidpw2en  7185  nnwetri  7189  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  tpfidisj  7202  tpfidceq  7203  exmidssfi  7212  iunfidisj  7226  mapfi  7227  fissfi  7229  snexxph  7233  fidcenumlemrks  7236  sbthlem2  7241  sbthlemi3  7242  sbthlem7  7246  sbthlemi8  7247  fival  7270  dcfi  7281  supmoti  7297  djuss  7374  updjudhf  7383  updjud  7386  casefun  7389  caseinj  7393  omp1eomlem  7398  djufun  7408  djuinj  7410  ctssdccl  7415  ctfoex  7422  nnnninf  7430  nnnninfeq2  7433  nninfisollem0  7434  nninfisollemne  7435  nninfisollemeq  7436  nninfisol  7437  finomni  7444  exmidomniim  7445  exmidomni  7446  fodjuomnilemdc  7448  omniwomnimkv  7471  nninfdcinf  7475  nninfwlporlem  7477  nninfwlpoimlemg  7479  nninfwlpoim  7483  nninfinfwlpo  7484  exmidonfinlem  7509  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  finacn  7524  exmidaclem  7528  dju1en  7533  exmidontriimlem1  7541  exmidontriimlem3  7543  iftrueb01  7546  pw1on  7549  3nsssucpw1  7559  2omotaplemap  7587  2omotap  7589  exmidmotap  7591  cc4f  7599  cc4n  7601  acnccim  7602  dmaddpqlem  7708  nqpi  7709  dmaddpq  7710  dmmulpq  7711  ltdcnq  7728  subhalfnqq  7745  enq0sym  7763  enq0ref  7764  enq0tr  7765  nqnq0pi  7769  nq0nn  7773  addnq0mo  7778  mulnq0mo  7779  nqpnq0nq  7784  nqnq0a  7785  nqnq0m  7786  npsspw  7802  elnp1st2nd  7807  prnmaxl  7819  prnminu  7820  prarloc  7834  genprndl  7852  genprndu  7853  nqprm  7873  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  prmuloc  7897  mulnqprlemrl  7904  mulnqprlemru  7905  ltsopr  7927  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  lteupri  7948  recexprlemopl  7956  recexprlemopu  7958  recexprlemdisj  7961  archpr  7974  cauappcvgprlemdisj  7982  cauappcvgprlemladdrl  7988  cauappcvgprlem2  7991  caucvgprlemnbj  7998  caucvgprlemdisj  8005  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemnbj  8024  caucvgprprlemdisj  8033  suplocexprlemml  8047  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemloc  8052  addsrmo  8074  mulsrmo  8075  recexgt0sr  8104  prsrpos  8116  caucvgsrlemasr  8121  suplocsrlemb  8137  suplocsrlempr  8138  suplocsr  8140  elrealeu  8160  pitonn  8179  pitoregt0  8180  pitore  8181  recnnre  8182  axaddcl  8195  axaddrcl  8196  axmulcl  8197  axmulrcl  8198  axrnegex  8210  axcnre  8212  axpre-lttrn  8215  rereceu  8220  axarch  8222  axpre-suploclemres  8232  axpre-suploc  8233  ltxrlt  8355  apirr  8896  divmulasscomap  8987  rerecclap  9021  lbreu  9236  arch  9510  0mnnnnn0  9545  nnm1nn0  9554  elnnnn0c  9558  elnnz1  9617  ztri3or0  9636  nzadd  9647  nn0n0n1ge2  9665  zdceq  9670  zdcle  9671  zdclt  9672  uzind  9707  eluzge3nn  9922  supinfneg  9945  infsupneg  9946  eluz2b2  9953  elnn1uz2  9957  elnn0dc  9961  elnndc  9962  nn01to3  9967  znq  9974  qaddcl  9985  qmulcl  9987  qreccl  9992  irradd  9996  irrmul  9997  elpq  9999  cnref1o  10001  xnn0dcle  10154  xrpnfdc  10194  xrmnfdc  10195  xaddcom  10213  xnegdi  10220  xpncan  10223  xleadd1a  10225  iooidg  10261  elioo4g  10286  elfzd  10369  fzdcel  10394  fznlem  10395  fzpreddisj  10427  fz0to4untppr  10480  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  elfzmlbp  10488  difelfzle  10490  4fvwrd4  10496  fzosplit  10535  elfzo0  10542  nn0p1elfzo  10543  fzo1fzo0n0  10544  elfzonn0  10547  fzofzim  10549  elfzo1  10552  elfzom1elp1fzo  10569  fzossfzop1  10579  ssfzo12bi  10592  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  qdceq  10628  qdclt  10629  exbtwnzlemstep  10631  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnxr  10641  modfzo0difsn  10781  frec2uzrand  10791  frec2uzf1od  10792  frecuzrdgrcl  10796  frecuzrdgtcl  10798  frecuzrdgrclt  10801  frecuzrdgfunlem  10805  frecfzennn  10812  nninfinf  10829  seq3f1olemp  10901  seq3f1oleml  10902  seqf1oglem1  10905  ser0f  10920  expcl2lemap  10937  hashunsng  11197  hashmap  11217  sshashneg  11230  hashfibclem  11231  hashfibc  11232  iswrdinn0  11254  snopiswrd  11259  wrdlndm  11266  iswrdsymb  11267  wrdsymb1  11286  ccatfv0  11316  ccatval21sw  11318  lswccatn0lsw  11324  eqs1  11341  ccat1st1st  11354  lswccats1fst  11357  fzowrddc  11364  swrdfv0  11371  swrdlen2  11379  swrdfv2  11380  swrdsbslen  11383  swrdspsleq  11384  pfxfv0  11409  pfxtrcfv0  11411  pfxeq  11413  pfx1  11420  swrdswrdlem  11421  cats1un  11438  pfxccatin12lem2a  11444  pfxccatin12lem2  11448  pfxccatin12lem3  11449  swrdccat  11452  cats1fvn  11481  cats1fvnd  11482  shftfvalg  11528  shftfval  11531  caucvgre  11691  rexanuz  11698  recvguniq  11705  rennim  11712  resqrexlemf  11717  rsqrmo  11737  fimaxre2  11937  climeu  12006  sumdc  12068  summodc  12094  zsumdc  12095  isum  12096  fisumss  12103  isumss2  12104  fsumsplit  12118  sumsnf  12120  fsumsplitsn  12121  sumtp  12125  sumsplitdc  12143  fsum2dlemstep  12145  fisum0diag2  12158  fsumconst  12165  modfsummodlemstep  12168  fsum00  12173  fsumabs  12176  fsumiun  12188  isumlessdc  12207  expcnv  12215  prodmodc  12289  zproddc  12290  iprodap  12291  iprodap0  12293  fprodssdc  12301  prodsnf  12303  fprodsplitdc  12307  fprodsplit  12308  fprodm1  12309  fprod1p  12310  fprodunsn  12315  fprod2dlemstep  12333  fprodsplitsn  12344  ef0lem  12371  modmulconst  12534  dvdsdivcl  12561  dvdsssfz1  12563  dvdsfac  12571  zeoxor  12580  nn0ehalf  12614  nn0oddm1d2  12620  nnoddm1d2  12621  divalglemeunn  12632  divalglemeuneg  12634  bitsfzolem  12665  bitsinv1  12673  gcdsupex  12678  gcdsupcl  12679  bezoutlemnewy  12717  bezoutlemmain  12719  bezoutlemeu  12728  dfgcd2  12735  nnwosdc  12760  nninfct  12762  algrf  12767  algcvgblem  12771  lcmgcdlem  12799  lcmdvds  12801  coprmgcdb  12810  mulgcddvds  12816  qredeu  12819  cncongr1  12825  cncongr2  12826  isprm2lem  12838  dvdsnprmd  12847  prmdc  12852  oddprmge3  12857  pw2dvdseu  12890  phibndlem  12938  dfphi2  12942  hashdvds  12943  phiprmpw  12944  eulerthlemh  12953  hashgcdeq  12962  phisum  12963  odzdvds  12968  reumodprminv  12976  nnnn0modprm0  12978  prm23ge5  12987  pclemdc  13011  pcdvdsb  13043  difsqpwdvds  13061  oddprmdvds  13077  1arith  13090  4sqlem3  13113  4sqlemafi  13118  4sqlemffi  13119  4sqleminfi  13120  4sqexercise1  13121  4sqlem11  13124  4sqlem19  13132  ballotfilemcdc  13167  ballotfilemdifcfi  13169  ballotfilemdifcfz  13171  ballotfilem2  13172  ballotfilemiex  13188  ballotfilemscl  13191  ballotfilemth  13225  ennnfonelemdc  13234  ennnfonelemh  13239  ennnfonelemhf1o  13248  ennnfonelemf1  13253  ennnfonelemrn  13254  ennnfonelemdm  13255  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctiunctlemudc  13272  ctiunctlemf  13273  ctiunctal  13276  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  isstructim  13310  setsresg  13334  strleund  13400  1strbas  13414  2strbasg  13417  2stropg  13418  restsspw  13546  tgval  13559  ptex  13561  imasaddfnlemg  13611  fnpr2o  13636  fnpr2ob  13637  mgmidsssn0  13681  fngsum  13685  igsumvalx  13686  isnsgrp  13703  sgrpidmndm  13717  mndinvmod  13742  mnd1  13752  mhmeql  13789  grpinveu  13835  prdsinvlem  13905  mulgval  13923  subgintm  13999  trivsubgsnd  14002  eqgfval  14023  ecqusaddd  14039  ecqusaddcl  14040  ghmeql  14068  iscmnd  14099  imasabl  14137  gsumfzmhm2  14145  rnglz  14173  srgfcl  14201  rhmopp  14406  opprlring  14427  subrgdvds  14466  lssuni  14623  lssintclm  14644  lspf  14649  qusmulrng  14792  mulgrhm2  14870  znf1o  14911  psrbagfi  14935  psrbagconcl  14939  psr1clfi  14955  mplsubgfilemcl  14966  istopon  14990  toponcom  15004  topgele  15006  topontopn  15014  tsettps  15015  eltg2b  15031  unitg  15039  tgss2  15056  bastop2  15061  distop  15062  epttop  15067  cldss2  15083  neisspw  15125  neipsm  15131  neiuni  15138  tgcn  15185  tgcnp  15186  cnntr  15202  lmff  15226  txuni2  15233  txbasex  15234  txbas  15235  txcnp  15248  txcnmpt  15250  txcn  15252  txdis  15254  txdis1cn  15255  cnmpt11  15260  cnmpt12  15264  cnmpt21  15268  cnmpt2t  15270  cnmpt22  15271  blsscls2  15470  xmetxpbl  15485  xmettxlem  15486  tgqioo  15532  fsumcncntop  15544  cncfmpt1f  15575  mulcncflem  15584  mulcncf  15585  dedekindeu  15600  dedekindicclemicc  15609  dedekindicc  15610  ivthinclemdisj  15617  hovercncf  15623  limcimo  15642  cnmptlimc  15651  reldvg  15656  dvfvalap  15658  dvfgg  15665  dvmptfsum  15702  dveflem  15703  dvef  15704  elply2  15712  sincn  15746  coscn  15747  reeff1o  15750  pilem3  15760  ioocosf1o  15831  mpodvdsmulf1o  15970  fsumdvdsmul  15971  perfectlem2  15980  lgsne0  16023  gausslemma2dlem1a  16043  gausslemma2dlem4  16049  lgseisenlem2  16056  lgseisenlem3  16057  lgsquadlem2  16063  2lgslem3  16086  2sqlem2  16100  mul2sq  16101  2sqlem3  16102  2sqlem7  16106  edgstruct  16171  pw0ss  16190  incistruhgr  16197  upgrex  16210  umgrnloop0  16224  upgr1een  16231  lfgrnloopen  16240  umgredg  16252  umgrnloop2  16258  uspgredgiedg  16285  uspgriedgedg  16286  usgrislfuspgrdom  16297  usgredg3  16321  uspgredg2vlem  16327  uspgredg2v  16328  ushgredgedg  16333  ushgredgedgloop  16335  uhgr0vsize0en  16342  usgr1e  16348  subusgr  16382  vtxedgfi  16396  vtxlpfi  16397  vtxdumgrfival  16405  1loopgrvd2fi  16412  p1evtxdeqfilem  16418  vdegp1aid  16421  wlkcprim  16457  wlk1walkdom  16466  uspgr2wlkeq  16472  upgr2wlkdc  16484  wlkres  16486  clwwlkccatlem  16507  clwwlknp  16524  umgr2cwwk2dif  16531  trlsegvdegfi  16574  eupth2lem3lem3fi  16577  eupth2lem3lem6fi  16578  eupth2lem3lem4fi  16580  eupth2lembfi  16584  depindlem1  16613  bj-trst  16623  bj-fast  16625  bj-stand  16632  bj-trdc  16636  bj-fadc  16638  decidr  16680  djulclALT  16685  djurclALT  16686  bj-charfunr  16692  bj-indind  16814  bj-2inf  16820  bj-nntrans2  16834  bj-peano4  16837  bj-nnord  16840  bj-inf2vn  16856  bj-inf2vn2  16857  bj-findis  16861  pwf1oexmid  16885  subctctexmid  16886  pw1dceq  16890  exmidnotnotr  16891  exmidcon  16892  exmidpeirce  16893  nnsf  16895  nninfsellemdc  16900  nninffeq  16910  nnnninfen  16911  exmidsbthrlem  16914  sbthom  16918  triap  16925  trilpo  16939  apdifflemr  16943  redcwlpo  16952  tridceq  16953  nconstwlpolem0  16961  nconstwlpolem  16963  nconstwlpo  16964  neapmkv  16966  ltlenmkv  16968  gfsump1  16980