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  3189  ssrdv  3190  3sstr4g  3227  eqsstrid  3230  ss2abdv  3257  abssdv  3258  rabssdv  3264  ss2rabdv  3265  ssun1  3327  unssad  3341  unssbd  3342  ssddif  3398  uneqin  3415  indifdir  3420  undif3ss  3425  reuss2  3444  n0rf  3464  reximdva0m  3467  rabxmdc  3483  ssindif0im  3511  minel  3513  ralidm  3552  ralm  3555  dcun  3561  ifmdc  3602  disjsn2  3686  absneu  3695  rabsneu  3696  opprc  3830  elunii  3845  dfnfc2  3858  uniss2  3871  unidif  3872  ssunieq  3873  intab  3904  iunss2  3962  iunssd  3963  iunxdif2  3966  invdisj  4028  disjiun  4029  3brtr4g  4068  trin  4142  triun  4145  truni  4146  trint  4147  iinexgm  4188  class2seteq  4197  pwuni  4226  exmid1dc  4234  exmidn0m  4235  exmidsssn  4236  exmid0el  4238  exmidel  4239  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  mss  4260  copsex2t  4279  euotd  4288  pwunim  4322  ispod  4340  sotricim  4359  exse  4372  frind  4388  trssord  4416  suctr  4457  pwnex  4485  eusvnf  4489  eusvnfb  4490  eusv2nf  4492  rexxfrd  4499  ralxfr2d  4500  rexxfr2d  4501  rabxfrd  4505  reuhypd  4507  eldifpw  4513  iunpw  4516  ssorduni  4524  onsucb  4540  onsucelsucr  4545  sucunielr  4547  ontriexmidim  4559  ordtri2or2exmidlem  4563  onsucelsucexmid  4567  reg2exmidlema  4571  setindel  4575  elirr  4578  orddisj  4583  en2lp  4591  suc11g  4594  ordsuc  4600  nlimsucg  4603  ordtri2or2exmid  4608  ontri2orexmidim  4609  zfregfr  4611  wessep  4615  tfi  4619  peano5  4635  limom  4651  peano2b  4652  nndceq0  4655  nnpredcl  4660  0nelrel  4710  eqrelrdv  4760  xpsspw  4776  relint  4788  relop  4817  eqbrrdva  4837  opeldm  4870  elres  4983  relssres  4985  elrelimasn  5036  exse2  5044  issref  5053  trin2  5062  dminss  5085  imainss  5086  rnxpid  5105  dmsn0el  5140  dmmptg  5168  relrelss  5197  cnviinm  5212  iotanul  5235  sniota  5250  dffun5r  5271  funmo  5274  funco  5299  funun  5303  funprg  5309  funtpg  5310  funtp  5312  fntpg  5315  fununi  5327  funcnvuni  5328  imadiflem  5338  imainlem  5340  funimaexglem  5342  isarep2  5346  fnunsn  5366  2elresin  5370  fnimadisj  5379  dmmptd  5389  fco  5424  funssxp  5428  fssres  5434  feu  5441  fimacnvdisj  5443  fabexg  5446  f00  5450  f0rn0  5453  f1co  5476  fores  5491  foco  5492  f1ores  5520  foimacnv  5523  f1oun  5525  fun11iun  5526  f1oco  5528  fo00  5541  brprcneu  5552  fv3  5582  relelfvdm  5591  nfvres  5593  nfunsn  5594  funfvbrb  5676  respreima  5691  dff2  5707  dff3im  5708  dffo4  5711  fvmptelcdm  5716  ffvresb  5726  f1oresrab  5728  fmptco  5729  fsn  5735  fpr  5745  ftpg  5747  fsnunf  5763  fsnunfv  5764  elabrex  5805  dff1o6  5824  foeqcnvco  5838  fliftel1  5842  isores1  5862  isoini2  5867  riotasbc  5894  acexmidlemph  5916  acexmidlemcase  5918  oprabidlem  5954  brabvv  5970  eloprabga  6011  fnoprabg  6025  caovimo  6119  oprabexd  6186  uchoice  6197  fo1stresm  6221  fo2ndresm  6222  unielxp  6234  1st2ndbr  6244  fmpoco  6276  1stconst  6281  2ndconst  6282  poxp  6292  spc2ed  6293  disjxp1  6296  reldmtpos  6313  tposfun  6320  dftpos4  6323  smores  6352  smores2  6354  tfrlem1  6368  tfr0dm  6382  tfrlemibxssdm  6387  tfrlemibex  6389  tfrlemiubacc  6390  tfrlemi14d  6393  tfrexlem  6394  tfri1d  6395  tfr1onlembxssdm  6403  tfr1onlembex  6405  tfr1onlemubacc  6406  tfr1onlemres  6409  tfrcllemsucfn  6413  tfrcllembxssdm  6416  tfrcllembex  6418  tfrcllemubacc  6419  tfrcllemres  6422  tfri3  6427  rdgon  6446  frecabcl  6459  frecfcllem  6464  frecrdg  6468  2oconcl  6499  nnsucelsuc  6551  nntri3or  6553  nndceq  6559  nndcel  6560  dcdifsnid  6564  ecexr  6599  brdifun  6621  ecelqsdm  6666  iinerm  6668  eroveu  6687  erovlem  6688  ecopovtrn  6693  ecopovtrng  6696  th3qlem1  6698  pmsspw  6744  map0b  6748  mapsn  6751  mapsncnv  6756  ixpf  6781  uniixp  6782  ixpexgg  6783  resixp  6794  f1oen3g  6815  ssdomg  6839  domtr  6846  snfig  6875  enpr2d  6878  xpf1o  6907  xpmapenlem  6912  php5dom  6926  fidceq  6932  nnfi  6935  fiunsnnn  6944  findcard  6951  findcard2  6952  findcard2s  6953  ac6sfi  6961  tridc  6962  fimax2gtri  6964  finexdc  6965  exmidpw  6971  exmidpweq  6972  exmidpw2en  6975  nnwetri  6979  unsnfi  6982  unsnfidcex  6983  unsnfidcel  6984  undifdcss  6986  tpfidisj  6992  tpfidceq  6993  iunfidisj  7014  snexxph  7018  fidcenumlemrks  7021  sbthlem2  7026  sbthlemi3  7027  sbthlem7  7031  sbthlemi8  7032  fival  7038  dcfi  7049  supmoti  7061  djuss  7138  updjudhf  7147  updjud  7150  casefun  7153  caseinj  7157  omp1eomlem  7162  djufun  7172  djuinj  7174  ctssdccl  7179  ctfoex  7186  nnnninf  7194  nnnninfeq2  7197  nninfisollem0  7198  nninfisollemne  7199  nninfisollemeq  7200  nninfisol  7201  finomni  7208  exmidomniim  7209  exmidomni  7210  fodjuomnilemdc  7212  omniwomnimkv  7235  nninfdcinf  7239  nninfwlporlem  7241  nninfwlpoimlemg  7243  nninfwlpoim  7246  exmidonfinlem  7263  exmidfodomrlemr  7272  exmidfodomrlemrALT  7273  exmidaclem  7278  dju1en  7283  exmidontriimlem1  7291  exmidontriimlem3  7293  pw1on  7296  3nsssucpw1  7306  2omotaplemap  7327  2omotap  7329  exmidmotap  7331  cc4f  7339  cc4n  7341  dmaddpqlem  7447  nqpi  7448  dmaddpq  7449  dmmulpq  7450  ltdcnq  7467  subhalfnqq  7484  enq0sym  7502  enq0ref  7503  enq0tr  7504  nqnq0pi  7508  nq0nn  7512  addnq0mo  7517  mulnq0mo  7518  nqpnq0nq  7523  nqnq0a  7524  nqnq0m  7525  npsspw  7541  elnp1st2nd  7546  prnmaxl  7558  prnminu  7559  prarloc  7573  genprndl  7591  genprndu  7592  nqprm  7612  nqprl  7621  nqpru  7622  addnqprlemrl  7627  addnqprlemru  7628  prmuloc  7636  mulnqprlemrl  7643  mulnqprlemru  7644  ltsopr  7666  ltexprlemm  7670  ltexprlemopl  7671  ltexprlemopu  7673  lteupri  7687  recexprlemopl  7695  recexprlemopu  7697  recexprlemdisj  7700  archpr  7713  cauappcvgprlemdisj  7721  cauappcvgprlemladdrl  7727  cauappcvgprlem2  7730  caucvgprlemnbj  7737  caucvgprlemdisj  7744  caucvgprlemladdfu  7747  caucvgprlem2  7750  caucvgprprlemnbj  7763  caucvgprprlemdisj  7772  suplocexprlemml  7786  suplocexprlemrl  7787  suplocexprlemmu  7788  suplocexprlemloc  7791  addsrmo  7813  mulsrmo  7814  recexgt0sr  7843  prsrpos  7855  caucvgsrlemasr  7860  suplocsrlemb  7876  suplocsrlempr  7877  suplocsr  7879  elrealeu  7899  pitonn  7918  pitoregt0  7919  pitore  7920  recnnre  7921  axaddcl  7934  axaddrcl  7935  axmulcl  7936  axmulrcl  7937  axrnegex  7949  axcnre  7951  axpre-lttrn  7954  rereceu  7959  axarch  7961  axpre-suploclemres  7971  axpre-suploc  7972  ltxrlt  8095  apirr  8635  divmulasscomap  8726  rerecclap  8760  lbreu  8975  arch  9249  0mnnnnn0  9284  nnm1nn0  9293  elnnnn0c  9297  elnnz1  9352  ztri3or0  9371  nzadd  9381  nn0n0n1ge2  9399  zdceq  9404  zdcle  9405  zdclt  9406  uzind  9440  eluzge3nn  9649  supinfneg  9672  infsupneg  9673  eluz2b2  9680  elnn1uz2  9684  elnn0dc  9688  elnndc  9689  nn01to3  9694  znq  9701  qaddcl  9712  qmulcl  9714  qreccl  9719  irradd  9723  irrmul  9724  elpq  9726  cnref1o  9728  xnn0dcle  9880  xrpnfdc  9920  xrmnfdc  9921  xaddcom  9939  xnegdi  9946  xpncan  9949  xleadd1a  9951  iooidg  9987  elioo4g  10012  elfzd  10094  fzdcel  10118  fznlem  10119  fzpreddisj  10149  fz0to4untppr  10202  elfz0ubfz0  10203  elfz0fzfz0  10204  fz0fzelfz0  10205  fz0fzdiffz0  10208  elfzmlbp  10210  difelfzle  10212  4fvwrd4  10218  fzosplit  10256  elfzo0  10261  fzo1fzo0n0  10262  elfzonn0  10265  fzofzim  10267  elfzo1  10269  elfzom1elp1fzo  10281  fzossfzop1  10291  ssfzo12bi  10304  exfzdc  10319  zsupcllemstep  10322  infssuzex  10326  qdceq  10337  qdclt  10338  exbtwnzlemstep  10340  exbtwnzlemex  10342  exbtwnz  10343  rebtwn2zlemstep  10345  rebtwn2z  10347  qbtwnxr  10350  modfzo0difsn  10490  frec2uzrand  10500  frec2uzf1od  10501  frecuzrdgrcl  10505  frecuzrdgtcl  10507  frecuzrdgrclt  10510  frecuzrdgfunlem  10514  frecfzennn  10521  nninfinf  10538  seq3f1olemp  10610  seq3f1oleml  10611  seqf1oglem1  10614  ser0f  10629  expcl2lemap  10646  hashunsng  10902  iswrdinn0  10943  snopiswrd  10948  wrdlndm  10955  iswrdsymb  10956  wrdsymb1  10974  shftfvalg  10986  shftfval  10989  caucvgre  11149  rexanuz  11156  recvguniq  11163  rennim  11170  resqrexlemf  11175  rsqrmo  11195  fimaxre2  11395  climeu  11464  sumdc  11526  summodc  11551  zsumdc  11552  isum  11553  fisumss  11560  isumss2  11561  fsumsplit  11575  sumsnf  11577  fsumsplitsn  11578  sumtp  11582  sumsplitdc  11600  fsum2dlemstep  11602  fisum0diag2  11615  fsumconst  11622  modfsummodlemstep  11625  fsum00  11630  fsumabs  11633  fsumiun  11645  isumlessdc  11664  expcnv  11672  prodmodc  11746  zproddc  11747  iprodap  11748  iprodap0  11750  fprodssdc  11758  prodsnf  11760  fprodsplitdc  11764  fprodsplit  11765  fprodm1  11766  fprod1p  11767  fprodunsn  11772  fprod2dlemstep  11790  fprodsplitsn  11801  ef0lem  11828  modmulconst  11991  dvdsdivcl  12018  dvdsssfz1  12020  dvdsfac  12028  zeoxor  12037  nn0ehalf  12071  nn0oddm1d2  12077  nnoddm1d2  12078  divalglemeunn  12089  divalglemeuneg  12091  bitsfzolem  12122  bitsinv1  12130  gcdsupex  12135  gcdsupcl  12136  bezoutlemnewy  12174  bezoutlemmain  12176  bezoutlemeu  12185  dfgcd2  12192  nnwosdc  12217  nninfct  12219  algrf  12224  algcvgblem  12228  lcmgcdlem  12256  lcmdvds  12258  coprmgcdb  12267  mulgcddvds  12273  qredeu  12276  cncongr1  12282  cncongr2  12283  isprm2lem  12295  dvdsnprmd  12304  prmdc  12309  oddprmge3  12314  pw2dvdseu  12347  phibndlem  12395  dfphi2  12399  hashdvds  12400  phiprmpw  12401  eulerthlemh  12410  hashgcdeq  12419  phisum  12420  odzdvds  12425  reumodprminv  12433  nnnn0modprm0  12435  prm23ge5  12444  pclemdc  12468  pcdvdsb  12500  difsqpwdvds  12518  oddprmdvds  12534  1arith  12547  4sqlem3  12570  4sqlemafi  12575  4sqlemffi  12576  4sqleminfi  12577  4sqexercise1  12578  4sqlem11  12581  4sqlem19  12589  ennnfonelemdc  12627  ennnfonelemh  12632  ennnfonelemhf1o  12641  ennnfonelemf1  12646  ennnfonelemrn  12647  ennnfonelemdm  12648  exmidunben  12654  ctinfomlemom  12655  ctinfom  12656  ctiunctlemudc  12665  ctiunctlemf  12666  ctiunctal  12669  nninfdclemcl  12676  nninfdclemf  12677  nninfdclemp1  12678  isstructim  12703  setsresg  12727  strleund  12792  1strbas  12806  2strbasg  12808  2stropg  12809  restsspw  12937  tgval  12950  ptex  12952  imasaddfnlemg  12983  fnpr2o  13008  fnpr2ob  13009  mgmidsssn0  13053  fngsum  13057  igsumvalx  13058  isnsgrp  13075  sgrpidmndm  13087  mndinvmod  13112  mnd1  13113  mhmeql  13150  grpinveu  13196  mulgval  13278  subgintm  13354  trivsubgsnd  13357  eqgfval  13378  ecqusaddd  13394  ecqusaddcl  13395  ghmeql  13423  iscmnd  13454  imasabl  13492  gsumfzmhm2  13500  rnglz  13527  srgfcl  13555  reldvdsrsrg  13674  rhmopp  13758  subrgdvds  13817  lssuni  13945  lssintclm  13966  lspf  13971  qusmulrng  14114  mulgrhm2  14192  znf1o  14233  istopon  14275  toponcom  14289  topgele  14291  topontopn  14299  tsettps  14300  eltg2b  14316  unitg  14324  tgss2  14341  bastop2  14346  distop  14347  epttop  14352  cldss2  14368  neisspw  14410  neipsm  14416  neiuni  14423  tgcn  14470  tgcnp  14471  cnntr  14487  lmff  14511  txuni2  14518  txbasex  14519  txbas  14520  txcnp  14533  txcnmpt  14535  txcn  14537  txdis  14539  txdis1cn  14540  cnmpt11  14545  cnmpt12  14549  cnmpt21  14553  cnmpt2t  14555  cnmpt22  14556  blsscls2  14755  xmetxpbl  14770  xmettxlem  14771  tgqioo  14817  fsumcncntop  14829  cncfmpt1f  14860  mulcncflem  14869  mulcncf  14870  dedekindeu  14885  dedekindicclemicc  14894  dedekindicc  14895  ivthinclemdisj  14902  hovercncf  14908  limcimo  14927  cnmptlimc  14936  reldvg  14941  dvfvalap  14943  dvfgg  14950  dvmptfsum  14987  dveflem  14988  dvef  14989  elply2  14997  sincn  15031  coscn  15032  reeff1o  15035  pilem3  15045  ioocosf1o  15116  mpodvdsmulf1o  15252  fsumdvdsmul  15253  perfectlem2  15262  lgsne0  15305  gausslemma2dlem1a  15325  gausslemma2dlem4  15331  lgseisenlem2  15338  lgseisenlem3  15339  lgsquadlem2  15345  2lgslem3  15368  2sqlem2  15382  mul2sq  15383  2sqlem3  15384  2sqlem7  15388  bj-trst  15411  bj-fast  15413  bj-stand  15420  bj-trdc  15424  bj-fadc  15426  decidr  15468  djulclALT  15473  djurclALT  15474  bj-charfunr  15482  bj-indind  15604  bj-2inf  15610  bj-nntrans2  15624  bj-peano4  15627  bj-nnord  15630  bj-inf2vn  15646  bj-inf2vn2  15647  bj-findis  15651  pwf1oexmid  15672  subctctexmid  15673  nnsf  15678  nninfsellemdc  15683  nninffeq  15693  nnnninfen  15694  exmidsbthrlem  15695  sbthom  15699  triap  15702  trilpo  15716  apdifflemr  15720  redcwlpo  15728  tridceq  15729  nconstwlpolem0  15736  nconstwlpolem  15738  nconstwlpo  15739  neapmkv  15741  ltlenmkv  15743