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  oibabs  715  dcim  842  dcstab  845  stdcndc  846  stdcndcOLD  847  dcand  934  dcor  937  3mix1  1168  3mix2  1169  3jca  1179  syl3anbrc  1183  syl21anbrc  1184  inegd  1383  pclem6  1385  xoranor  1388  dcfrompeirce  1460  nfxfrd  1489  nfd  1537  hban  1561  nfan1  1578  nford  1581  nfand  1582  hbim1  1584  nfal  1590  alexim  1659  nnal  1663  ax6blem  1664  nf4r  1685  19.34  1698  nfexd  1775  sbcof2  1824  nfsb2or  1851  sbidm  1865  nfdv  1891  nfd2  2041  nfeudv  2060  mon  2074  eumo  2077  mo23  2086  eu2  2089  eu3h  2090  exmodc  2095  exmonim  2096  mo2r  2097  mo3h  2098  bm1.1  2181  eqrdv  2194  3eltr4g  2282  abbi2dv  2315  abbi1dv  2316  nfcd  2334  nfcxfrd  2337  dcned  2373  neqned  2374  3netr4g  2402  necon3bi  2417  necon2ai  2421  nnral  2487  alral  2542  rspe  2546  rsp2e  2548  rgen2a  2551  ralrimi  2568  r19.27v  2624  r19.28v  2625  r19.27av  2632  r19.32r  2643  nfreudxy  2671  mormo  2713  nrexrmo  2718  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  rspce  2863  ceqex  2891  elrab3t  2919  elrabd  2922  mosubt  2941  mo2icl  2943  reu3  2954  reu6i  2955  2rmorex  2970  sbc5  3013  rspesbca  3074  rmo2ilem  3079  sbnfc2  3145  ssrd  3188  ssrdv  3189  3sstr4g  3226  eqsstrid  3229  ss2abdv  3256  abssdv  3257  rabssdv  3263  ss2rabdv  3264  ssun1  3326  unssad  3340  unssbd  3341  ssddif  3397  uneqin  3414  indifdir  3419  undif3ss  3424  reuss2  3443  n0rf  3463  reximdva0m  3466  rabxmdc  3482  ssindif0im  3510  minel  3512  ralidm  3551  ralm  3554  dcun  3560  ifmdc  3601  disjsn2  3685  absneu  3694  rabsneu  3695  opprc  3829  elunii  3844  dfnfc2  3857  uniss2  3870  unidif  3871  ssunieq  3872  intab  3903  iunss2  3961  iunssd  3962  iunxdif2  3965  invdisj  4027  disjiun  4028  3brtr4g  4067  trin  4141  triun  4144  truni  4145  trint  4146  iinexgm  4187  class2seteq  4196  pwuni  4225  exmid1dc  4233  exmidn0m  4234  exmidsssn  4235  exmid0el  4237  exmidel  4238  exmidundif  4239  exmidundifim  4240  exmid1stab  4241  mss  4259  copsex2t  4278  euotd  4287  pwunim  4321  ispod  4339  sotricim  4358  exse  4371  frind  4387  trssord  4415  suctr  4456  pwnex  4484  eusvnf  4488  eusvnfb  4489  eusv2nf  4491  rexxfrd  4498  ralxfr2d  4499  rexxfr2d  4500  rabxfrd  4504  reuhypd  4506  eldifpw  4512  iunpw  4515  ssorduni  4523  onsucb  4539  onsucelsucr  4544  sucunielr  4546  ontriexmidim  4558  ordtri2or2exmidlem  4562  onsucelsucexmid  4566  reg2exmidlema  4570  setindel  4574  elirr  4577  orddisj  4582  en2lp  4590  suc11g  4593  ordsuc  4599  nlimsucg  4602  ordtri2or2exmid  4607  ontri2orexmidim  4608  zfregfr  4610  wessep  4614  tfi  4618  peano5  4634  limom  4650  peano2b  4651  nndceq0  4654  nnpredcl  4659  0nelrel  4709  eqrelrdv  4759  xpsspw  4775  relint  4787  relop  4816  eqbrrdva  4836  opeldm  4869  elres  4982  relssres  4984  elrelimasn  5035  exse2  5043  issref  5052  trin2  5061  dminss  5084  imainss  5085  rnxpid  5104  dmsn0el  5139  dmmptg  5167  relrelss  5196  cnviinm  5211  iotanul  5234  sniota  5249  dffun5r  5270  funmo  5273  funco  5298  funun  5302  funprg  5308  funtpg  5309  funtp  5311  fntpg  5314  fununi  5326  funcnvuni  5327  imadiflem  5337  imainlem  5339  funimaexglem  5341  isarep2  5345  fnunsn  5365  2elresin  5369  fnimadisj  5378  dmmptd  5388  fco  5423  funssxp  5427  fssres  5433  feu  5440  fimacnvdisj  5442  fabexg  5445  f00  5449  f0rn0  5452  f1co  5475  fores  5490  foco  5491  f1ores  5519  foimacnv  5522  f1oun  5524  fun11iun  5525  f1oco  5527  fo00  5540  brprcneu  5551  fv3  5581  relelfvdm  5590  nfvres  5592  nfunsn  5593  funfvbrb  5675  respreima  5690  dff2  5706  dff3im  5707  dffo4  5710  fvmptelcdm  5715  ffvresb  5725  f1oresrab  5727  fmptco  5728  fsn  5734  fpr  5744  ftpg  5746  fsnunf  5762  fsnunfv  5763  elabrex  5804  dff1o6  5823  foeqcnvco  5837  fliftel1  5841  isores1  5861  isoini2  5866  riotasbc  5893  acexmidlemph  5915  acexmidlemcase  5917  oprabidlem  5953  brabvv  5968  eloprabga  6009  fnoprabg  6023  caovimo  6117  oprabexd  6184  uchoice  6195  fo1stresm  6219  fo2ndresm  6220  unielxp  6232  1st2ndbr  6242  fmpoco  6274  1stconst  6279  2ndconst  6280  poxp  6290  spc2ed  6291  disjxp1  6294  reldmtpos  6311  tposfun  6318  dftpos4  6321  smores  6350  smores2  6352  tfrlem1  6366  tfr0dm  6380  tfrlemibxssdm  6385  tfrlemibex  6387  tfrlemiubacc  6388  tfrlemi14d  6391  tfrexlem  6392  tfri1d  6393  tfr1onlembxssdm  6401  tfr1onlembex  6403  tfr1onlemubacc  6404  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllembxssdm  6414  tfrcllembex  6416  tfrcllemubacc  6417  tfrcllemres  6420  tfri3  6425  rdgon  6444  frecabcl  6457  frecfcllem  6462  frecrdg  6466  2oconcl  6497  nnsucelsuc  6549  nntri3or  6551  nndceq  6557  nndcel  6558  dcdifsnid  6562  ecexr  6597  brdifun  6619  ecelqsdm  6664  iinerm  6666  eroveu  6685  erovlem  6686  ecopovtrn  6691  ecopovtrng  6694  th3qlem1  6696  pmsspw  6742  map0b  6746  mapsn  6749  mapsncnv  6754  ixpf  6779  uniixp  6780  ixpexgg  6781  resixp  6792  f1oen3g  6813  ssdomg  6837  domtr  6844  snfig  6873  enpr2d  6876  xpf1o  6905  xpmapenlem  6910  php5dom  6924  fidceq  6930  nnfi  6933  fiunsnnn  6942  findcard  6949  findcard2  6950  findcard2s  6951  ac6sfi  6959  tridc  6960  fimax2gtri  6962  finexdc  6963  exmidpw  6969  exmidpweq  6970  exmidpw2en  6973  nnwetri  6977  unsnfi  6980  unsnfidcex  6981  unsnfidcel  6982  undifdcss  6984  tpfidisj  6990  tpfidceq  6991  iunfidisj  7012  snexxph  7016  fidcenumlemrks  7019  sbthlem2  7024  sbthlemi3  7025  sbthlem7  7029  sbthlemi8  7030  fival  7036  dcfi  7047  supmoti  7059  djuss  7136  updjudhf  7145  updjud  7148  casefun  7151  caseinj  7155  omp1eomlem  7160  djufun  7170  djuinj  7172  ctssdccl  7177  ctfoex  7184  nnnninf  7192  nnnninfeq2  7195  nninfisollem0  7196  nninfisollemne  7197  nninfisollemeq  7198  nninfisol  7199  finomni  7206  exmidomniim  7207  exmidomni  7208  fodjuomnilemdc  7210  omniwomnimkv  7233  nninfdcinf  7237  nninfwlporlem  7239  nninfwlpoimlemg  7241  nninfwlpoim  7244  exmidonfinlem  7260  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  dju1en  7280  exmidontriimlem1  7288  exmidontriimlem3  7290  pw1on  7293  3nsssucpw1  7303  2omotaplemap  7324  2omotap  7326  exmidmotap  7328  cc4f  7336  cc4n  7338  dmaddpqlem  7444  nqpi  7445  dmaddpq  7446  dmmulpq  7447  ltdcnq  7464  subhalfnqq  7481  enq0sym  7499  enq0ref  7500  enq0tr  7501  nqnq0pi  7505  nq0nn  7509  addnq0mo  7514  mulnq0mo  7515  nqpnq0nq  7520  nqnq0a  7521  nqnq0m  7522  npsspw  7538  elnp1st2nd  7543  prnmaxl  7555  prnminu  7556  prarloc  7570  genprndl  7588  genprndu  7589  nqprm  7609  nqprl  7618  nqpru  7619  addnqprlemrl  7624  addnqprlemru  7625  prmuloc  7633  mulnqprlemrl  7640  mulnqprlemru  7641  ltsopr  7663  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  lteupri  7684  recexprlemopl  7692  recexprlemopu  7694  recexprlemdisj  7697  archpr  7710  cauappcvgprlemdisj  7718  cauappcvgprlemladdrl  7724  cauappcvgprlem2  7727  caucvgprlemnbj  7734  caucvgprlemdisj  7741  caucvgprlemladdfu  7744  caucvgprlem2  7747  caucvgprprlemnbj  7760  caucvgprprlemdisj  7769  suplocexprlemml  7783  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemloc  7788  addsrmo  7810  mulsrmo  7811  recexgt0sr  7840  prsrpos  7852  caucvgsrlemasr  7857  suplocsrlemb  7873  suplocsrlempr  7874  suplocsr  7876  elrealeu  7896  pitonn  7915  pitoregt0  7916  pitore  7917  recnnre  7918  axaddcl  7931  axaddrcl  7932  axmulcl  7933  axmulrcl  7934  axrnegex  7946  axcnre  7948  axpre-lttrn  7951  rereceu  7956  axarch  7958  axpre-suploclemres  7968  axpre-suploc  7969  ltxrlt  8092  apirr  8632  divmulasscomap  8723  rerecclap  8757  lbreu  8972  arch  9246  0mnnnnn0  9281  nnm1nn0  9290  elnnnn0c  9294  elnnz1  9349  ztri3or0  9368  nzadd  9378  nn0n0n1ge2  9396  zdceq  9401  zdcle  9402  zdclt  9403  uzind  9437  eluzge3nn  9646  supinfneg  9669  infsupneg  9670  eluz2b2  9677  elnn1uz2  9681  elnn0dc  9685  elnndc  9686  nn01to3  9691  znq  9698  qaddcl  9709  qmulcl  9711  qreccl  9716  irradd  9720  irrmul  9721  elpq  9723  cnref1o  9725  xnn0dcle  9877  xrpnfdc  9917  xrmnfdc  9918  xaddcom  9936  xnegdi  9943  xpncan  9946  xleadd1a  9948  iooidg  9984  elioo4g  10009  elfzd  10091  fzdcel  10115  fznlem  10116  fzpreddisj  10146  fz0to4untppr  10199  elfz0ubfz0  10200  elfz0fzfz0  10201  fz0fzelfz0  10202  fz0fzdiffz0  10205  elfzmlbp  10207  difelfzle  10209  4fvwrd4  10215  fzosplit  10253  elfzo0  10258  fzo1fzo0n0  10259  elfzonn0  10262  fzofzim  10264  elfzo1  10266  elfzom1elp1fzo  10278  fzossfzop1  10288  ssfzo12bi  10301  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  qdceq  10334  qdclt  10335  exbtwnzlemstep  10337  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2z  10344  qbtwnxr  10347  modfzo0difsn  10487  frec2uzrand  10497  frec2uzf1od  10498  frecuzrdgrcl  10502  frecuzrdgtcl  10504  frecuzrdgrclt  10507  frecuzrdgfunlem  10511  frecfzennn  10518  nninfinf  10535  seq3f1olemp  10607  seq3f1oleml  10608  seqf1oglem1  10611  ser0f  10626  expcl2lemap  10643  hashunsng  10899  iswrdinn0  10940  snopiswrd  10945  wrdlndm  10952  iswrdsymb  10953  wrdsymb1  10971  shftfvalg  10983  shftfval  10986  caucvgre  11146  rexanuz  11153  recvguniq  11160  rennim  11167  resqrexlemf  11172  rsqrmo  11192  fimaxre2  11392  climeu  11461  sumdc  11523  summodc  11548  zsumdc  11549  isum  11550  fisumss  11557  isumss2  11558  fsumsplit  11572  sumsnf  11574  fsumsplitsn  11575  sumtp  11579  sumsplitdc  11597  fsum2dlemstep  11599  fisum0diag2  11612  fsumconst  11619  modfsummodlemstep  11622  fsum00  11627  fsumabs  11630  fsumiun  11642  isumlessdc  11661  expcnv  11669  prodmodc  11743  zproddc  11744  iprodap  11745  iprodap0  11747  fprodssdc  11755  prodsnf  11757  fprodsplitdc  11761  fprodsplit  11762  fprodm1  11763  fprod1p  11764  fprodunsn  11769  fprod2dlemstep  11787  fprodsplitsn  11798  ef0lem  11825  modmulconst  11988  dvdsdivcl  12015  dvdsssfz1  12017  dvdsfac  12025  zeoxor  12034  nn0ehalf  12068  nn0oddm1d2  12074  nnoddm1d2  12075  divalglemeunn  12086  divalglemeuneg  12088  bitsfzolem  12118  gcdsupex  12124  gcdsupcl  12125  bezoutlemnewy  12163  bezoutlemmain  12165  bezoutlemeu  12174  dfgcd2  12181  nnwosdc  12206  nninfct  12208  algrf  12213  algcvgblem  12217  lcmgcdlem  12245  lcmdvds  12247  coprmgcdb  12256  mulgcddvds  12262  qredeu  12265  cncongr1  12271  cncongr2  12272  isprm2lem  12284  dvdsnprmd  12293  prmdc  12298  oddprmge3  12303  pw2dvdseu  12336  phibndlem  12384  dfphi2  12388  hashdvds  12389  phiprmpw  12390  eulerthlemh  12399  hashgcdeq  12408  phisum  12409  odzdvds  12414  reumodprminv  12422  nnnn0modprm0  12424  prm23ge5  12433  pclemdc  12457  pcdvdsb  12489  difsqpwdvds  12507  oddprmdvds  12523  1arith  12536  4sqlem3  12559  4sqlemafi  12564  4sqlemffi  12565  4sqleminfi  12566  4sqexercise1  12567  4sqlem11  12570  4sqlem19  12578  ennnfonelemdc  12616  ennnfonelemh  12621  ennnfonelemhf1o  12630  ennnfonelemf1  12635  ennnfonelemrn  12636  ennnfonelemdm  12637  exmidunben  12643  ctinfomlemom  12644  ctinfom  12645  ctiunctlemudc  12654  ctiunctlemf  12655  ctiunctal  12658  nninfdclemcl  12665  nninfdclemf  12666  nninfdclemp1  12667  isstructim  12692  setsresg  12716  strleund  12781  1strbas  12795  2strbasg  12797  2stropg  12798  restsspw  12920  tgval  12933  ptex  12935  imasaddfnlemg  12957  fnpr2o  12982  fnpr2ob  12983  mgmidsssn0  13027  fngsum  13031  igsumvalx  13032  isnsgrp  13049  sgrpidmndm  13061  mndinvmod  13086  mnd1  13087  mhmeql  13124  grpinveu  13170  mulgval  13252  subgintm  13328  trivsubgsnd  13331  eqgfval  13352  ecqusaddd  13368  ecqusaddcl  13369  ghmeql  13397  iscmnd  13428  imasabl  13466  gsumfzmhm2  13474  rnglz  13501  srgfcl  13529  reldvdsrsrg  13648  rhmopp  13732  subrgdvds  13791  lssuni  13919  lssintclm  13940  lspf  13945  qusmulrng  14088  mulgrhm2  14166  znf1o  14207  istopon  14249  toponcom  14263  topgele  14265  topontopn  14273  tsettps  14274  eltg2b  14290  unitg  14298  tgss2  14315  bastop2  14320  distop  14321  epttop  14326  cldss2  14342  neisspw  14384  neipsm  14390  neiuni  14397  tgcn  14444  tgcnp  14445  cnntr  14461  lmff  14485  txuni2  14492  txbasex  14493  txbas  14494  txcnp  14507  txcnmpt  14509  txcn  14511  txdis  14513  txdis1cn  14514  cnmpt11  14519  cnmpt12  14523  cnmpt21  14527  cnmpt2t  14529  cnmpt22  14530  blsscls2  14729  xmetxpbl  14744  xmettxlem  14745  tgqioo  14791  fsumcncntop  14803  cncfmpt1f  14834  mulcncflem  14843  mulcncf  14844  dedekindeu  14859  dedekindicclemicc  14868  dedekindicc  14869  ivthinclemdisj  14876  hovercncf  14882  limcimo  14901  cnmptlimc  14910  reldvg  14915  dvfvalap  14917  dvfgg  14924  dvmptfsum  14961  dveflem  14962  dvef  14963  elply2  14971  sincn  15005  coscn  15006  reeff1o  15009  pilem3  15019  ioocosf1o  15090  mpodvdsmulf1o  15226  fsumdvdsmul  15227  perfectlem2  15236  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem4  15305  lgseisenlem2  15312  lgseisenlem3  15313  lgsquadlem2  15319  2lgslem3  15342  2sqlem2  15356  mul2sq  15357  2sqlem3  15358  2sqlem7  15362  bj-trst  15385  bj-fast  15387  bj-stand  15394  bj-trdc  15398  bj-fadc  15400  decidr  15442  djulclALT  15447  djurclALT  15448  bj-charfunr  15456  bj-indind  15578  bj-2inf  15584  bj-nntrans2  15598  bj-peano4  15601  bj-nnord  15604  bj-inf2vn  15620  bj-inf2vn2  15621  bj-findis  15625  pwf1oexmid  15644  subctctexmid  15645  nnsf  15649  nninfsellemdc  15654  nninffeq  15664  nnnninfen  15665  exmidsbthrlem  15666  sbthom  15670  triap  15673  trilpo  15687  apdifflemr  15691  redcwlpo  15699  tridceq  15700  nconstwlpolem0  15707  nconstwlpolem  15709  nconstwlpo  15710  neapmkv  15712  ltlenmkv  15714