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  8897  divmulasscomap  8990  rerecclap  9024  lbreu  9239  arch  9513  0mnnnnn0  9548  nnm1nn0  9557  elnnnn0c  9561  elnnz1  9620  ztri3or0  9639  nzadd  9650  nn0n0n1ge2  9668  zdceq  9673  zdcle  9674  zdclt  9675  uzind  9710  eluzge3nn  9925  supinfneg  9948  infsupneg  9949  eluz2b2  9956  elnn1uz2  9960  elnn0dc  9964  elnndc  9965  nn01to3  9970  znq  9977  qaddcl  9988  qmulcl  9990  qreccl  9995  irradd  9999  irrmul  10000  elpq  10002  cnref1o  10004  xnn0dcle  10157  xrpnfdc  10197  xrmnfdc  10198  xaddcom  10216  xnegdi  10223  xpncan  10226  xleadd1a  10228  iooidg  10264  elioo4g  10289  elfzd  10372  fzdcel  10397  fznlem  10398  fzpreddisj  10430  fz0to4untppr  10483  elfz0ubfz0  10484  elfz0fzfz0  10485  fz0fzelfz0  10486  fz0fzdiffz0  10489  elfzmlbp  10491  difelfzle  10493  4fvwrd4  10499  fzosplit  10538  elfzo0  10545  nn0p1elfzo  10546  fzo1fzo0n0  10547  elfzonn0  10550  fzofzim  10552  elfzo1  10555  elfzom1elp1fzo  10572  fzossfzop1  10582  ssfzo12bi  10595  exfzdc  10611  zsupcllemstep  10614  infssuzex  10618  qdceq  10631  qdclt  10632  exbtwnzlemstep  10634  exbtwnzlemex  10636  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  qbtwnxr  10644  modfzo0difsn  10784  frec2uzrand  10794  frec2uzf1od  10795  frecuzrdgrcl  10799  frecuzrdgtcl  10801  frecuzrdgrclt  10804  frecuzrdgfunlem  10808  frecfzennn  10815  nninfinf  10832  seq3f1olemp  10904  seq3f1oleml  10905  seqf1oglem1  10908  ser0f  10923  expcl2lemap  10940  hashunsng  11200  hashmap  11220  sshashneg  11233  hashfibclem  11234  hashfibc  11235  iswrdinn0  11257  snopiswrd  11262  wrdlndm  11269  iswrdsymb  11270  wrdsymb1  11289  ccatfv0  11319  ccatval21sw  11321  lswccatn0lsw  11327  eqs1  11344  ccat1st1st  11357  lswccats1fst  11360  fzowrddc  11367  swrdfv0  11374  swrdlen2  11382  swrdfv2  11383  swrdsbslen  11386  swrdspsleq  11387  pfxfv0  11412  pfxtrcfv0  11414  pfxeq  11416  pfx1  11423  swrdswrdlem  11424  cats1un  11441  pfxccatin12lem2a  11447  pfxccatin12lem2  11451  pfxccatin12lem3  11452  swrdccat  11455  cats1fvn  11484  cats1fvnd  11485  shftfvalg  11531  shftfval  11534  caucvgre  11695  rexanuz  11702  recvguniq  11709  rennim  11716  resqrexlemf  11721  rsqrmo  11741  fimaxre2  11941  climeu  12010  sumdc  12072  summodc  12098  zsumdc  12099  isum  12100  fisumss  12107  isumss2  12108  fsumsplit  12122  sumsnf  12124  fsumsplitsn  12125  sumtp  12129  sumsplitdc  12147  fsum2dlemstep  12149  fisum0diag2  12162  fsumconst  12169  modfsummodlemstep  12172  fsum00  12177  fsumabs  12180  fsumiun  12192  isumlessdc  12211  expcnv  12219  prodmodc  12293  zproddc  12294  iprodap  12295  iprodap0  12297  fprodssdc  12305  prodsnf  12307  fprodsplitdc  12311  fprodsplit  12312  fprodm1  12313  fprod1p  12314  fprodunsn  12319  fprod2dlemstep  12337  fprodsplitsn  12348  ef0lem  12375  modmulconst  12538  dvdsdivcl  12565  dvdsssfz1  12567  dvdsfac  12575  zeoxor  12584  nn0ehalf  12618  nn0oddm1d2  12624  nnoddm1d2  12625  divalglemeunn  12636  divalglemeuneg  12638  bitsfzolem  12669  bitsinv1  12677  gcdsupex  12682  gcdsupcl  12683  bezoutlemnewy  12721  bezoutlemmain  12723  bezoutlemeu  12732  dfgcd2  12739  nnwosdc  12764  nninfct  12766  algrf  12771  algcvgblem  12775  lcmgcdlem  12803  lcmdvds  12805  coprmgcdb  12814  mulgcddvds  12820  qredeu  12823  cncongr1  12829  cncongr2  12830  isprm2lem  12842  dvdsnprmd  12851  prmdc  12856  oddprmge3  12861  pw2dvdseu  12894  phibndlem  12942  dfphi2  12946  hashdvds  12947  phiprmpw  12948  eulerthlemh  12957  hashgcdeq  12966  phisum  12967  odzdvds  12972  reumodprminv  12980  nnnn0modprm0  12982  prm23ge5  12991  pclemdc  13015  pcdvdsb  13047  difsqpwdvds  13065  oddprmdvds  13081  1arith  13094  4sqlem3  13117  4sqlemafi  13122  4sqlemffi  13123  4sqleminfi  13124  4sqexercise1  13125  4sqlem11  13128  4sqlem19  13136  ballotfilemcdc  13171  ballotfilemdifcfi  13173  ballotfilemdifcfz  13175  ballotfilem2  13176  ballotfilemiex  13192  ballotfilemscl  13195  ballotfilemth  13229  ennnfonelemdc  13238  ennnfonelemh  13243  ennnfonelemhf1o  13252  ennnfonelemf1  13257  ennnfonelemrn  13258  ennnfonelemdm  13259  exmidunben  13265  ctinfomlemom  13266  ctinfom  13267  ctiunctlemudc  13276  ctiunctlemf  13277  ctiunctal  13280  nninfdclemcl  13287  nninfdclemf  13288  nninfdclemp1  13289  isstructim  13314  setsresg  13338  strleund  13404  1strbas  13418  2strbasg  13421  2stropg  13422  restsspw  13550  tgval  13563  ptex  13565  imasaddfnlemg  13582  fnpr2o  13607  fnpr2ob  13608  mgmidsssn0  13651  fngsum  13655  igsumvalx  13656  isnsgrp  13673  sgrpidmndm  13685  mndinvmod  13710  mnd1  13714  mhmeql  13751  grpinveu  13797  mulgval  13879  subgintm  13955  trivsubgsnd  13958  eqgfval  13979  ecqusaddd  13995  ecqusaddcl  13996  ghmeql  14024  iscmnd  14055  imasabl  14093  gsumfzmhm2  14101  gfsump1  14112  prdsinvlem  14142  rnglz  14188  srgfcl  14220  rhmopp  14425  opprlring  14446  subrgdvds  14485  lssuni  14641  lssintclm  14662  lspf  14667  qusmulrng  14810  mulgrhm2  14888  znf1o  14929  psrbagfi  14953  psrbagconcl  14957  psr1clfi  14973  mplsubgfilemcl  14984  istopon  15008  toponcom  15022  topgele  15024  topontopn  15032  tsettps  15033  eltg2b  15049  unitg  15057  tgss2  15074  bastop2  15079  distop  15080  epttop  15085  cldss2  15101  neisspw  15143  neipsm  15149  neiuni  15156  tgcn  15203  tgcnp  15204  cnntr  15220  lmff  15244  txuni2  15251  txbasex  15252  txbas  15253  txcnp  15266  txcnmpt  15268  txcn  15270  txdis  15272  txdis1cn  15273  cnmpt11  15278  cnmpt12  15282  cnmpt21  15286  cnmpt2t  15288  cnmpt22  15289  blsscls2  15488  xmetxpbl  15503  xmettxlem  15504  tgqioo  15550  fsumcncntop  15562  cncfmpt1f  15593  mulcncflem  15602  mulcncf  15603  dedekindeu  15618  dedekindicclemicc  15627  dedekindicc  15628  ivthinclemdisj  15635  hovercncf  15641  limcimo  15660  cnmptlimc  15669  reldvg  15674  dvfvalap  15676  dvfgg  15683  dvmptfsum  15720  dveflem  15721  dvef  15722  elply2  15730  sincn  15764  coscn  15765  reeff1o  15768  pilem3  15778  ioocosf1o  15849  mpodvdsmulf1o  15988  fsumdvdsmul  15989  perfectlem2  15998  lgsne0  16041  gausslemma2dlem1a  16061  gausslemma2dlem4  16067  lgseisenlem2  16074  lgseisenlem3  16075  lgsquadlem2  16081  2lgslem3  16104  2sqlem2  16118  mul2sq  16119  2sqlem3  16120  2sqlem7  16124  edgstruct  16189  pw0ss  16208  incistruhgr  16215  upgrex  16228  umgrnloop0  16242  upgr1een  16249  lfgrnloopen  16258  umgredg  16270  umgrnloop2  16276  uspgredgiedg  16303  uspgriedgedg  16304  usgrislfuspgrdom  16315  usgredg3  16339  uspgredg2vlem  16345  uspgredg2v  16346  ushgredgedg  16351  ushgredgedgloop  16353  uhgr0vsize0en  16360  usgr1e  16366  subusgr  16400  vtxedgfi  16414  vtxlpfi  16415  vtxdumgrfival  16423  1loopgrvd2fi  16430  p1evtxdeqfilem  16436  vdegp1aid  16439  wlkcprim  16475  wlk1walkdom  16484  uspgr2wlkeq  16490  upgr2wlkdc  16502  wlkres  16504  clwwlkccatlem  16525  clwwlknp  16542  umgr2cwwk2dif  16549  trlsegvdegfi  16592  eupth2lem3lem3fi  16595  eupth2lem3lem6fi  16596  eupth2lem3lem4fi  16598  eupth2lembfi  16602  depindlem1  16631  bj-trst  16651  bj-fast  16653  bj-stand  16660  bj-trdc  16664  bj-fadc  16666  decidr  16708  djulclALT  16713  djurclALT  16714  bj-charfunr  16720  bj-indind  16842  bj-2inf  16848  bj-nntrans2  16862  bj-peano4  16865  bj-nnord  16868  bj-inf2vn  16884  bj-inf2vn2  16885  bj-findis  16889  pwf1oexmid  16913  subctctexmid  16914  pw1dceq  16918  exmidnotnotr  16919  exmidcon  16920  exmidpeirce  16921  nnsf  16923  nninfsellemdc  16928  nninffeq  16938  nnnninfen  16939  exmidsbthrlem  16942  sbthom  16946  triap  16953  trilpo  16967  apdifflemr  16971  redcwlpo  16980  tridceq  16981  nconstwlpolem0  16988  nconstwlpolem  16990  nconstwlpo  16991  neapmkv  16993  ltlenmkv  16995