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  nfxfrd  1486  nfd  1534  hban  1558  nfan1  1575  nford  1578  nfand  1579  hbim1  1581  nfal  1587  alexim  1656  nnal  1660  ax6blem  1661  nf4r  1682  19.34  1695  nfexd  1772  sbcof2  1821  nfsb2or  1848  sbidm  1862  nfdv  1888  nfd2  2038  nfeudv  2057  mon  2071  eumo  2074  mo23  2083  eu2  2086  eu3h  2087  exmodc  2092  exmonim  2093  mo2r  2094  mo3h  2095  bm1.1  2178  eqrdv  2191  3eltr4g  2279  abbi2dv  2312  abbi1dv  2313  nfcd  2331  nfcxfrd  2334  dcned  2370  neqned  2371  3netr4g  2399  necon3bi  2414  necon2ai  2418  nnral  2484  alral  2539  rspe  2543  rsp2e  2545  rgen2a  2548  ralrimi  2565  r19.27v  2621  r19.28v  2622  r19.27av  2629  r19.32r  2640  nfreudxy  2668  mormo  2710  nrexrmo  2715  cgsex2g  2796  cgsex4g  2797  spc2egv  2851  spc2gv  2852  spc3egv  2853  spc3gv  2854  rspce  2860  ceqex  2888  elrab3t  2916  elrabd  2919  mosubt  2938  mo2icl  2940  reu3  2951  reu6i  2952  2rmorex  2967  sbc5  3010  rspesbca  3071  rmo2ilem  3076  sbnfc2  3142  ssrd  3185  ssrdv  3186  3sstr4g  3223  eqsstrid  3226  ss2abdv  3253  abssdv  3254  rabssdv  3260  ss2rabdv  3261  ssun1  3323  unssad  3337  unssbd  3338  ssddif  3394  uneqin  3411  indifdir  3416  undif3ss  3421  reuss2  3440  n0rf  3460  reximdva0m  3463  rabxmdc  3479  ssindif0im  3507  minel  3509  ralidm  3548  ralm  3551  dcun  3557  ifmdc  3598  disjsn2  3682  absneu  3691  rabsneu  3692  opprc  3826  elunii  3841  dfnfc2  3854  uniss2  3867  unidif  3868  ssunieq  3869  intab  3900  iunss2  3958  iunssd  3959  iunxdif2  3962  invdisj  4024  disjiun  4025  3brtr4g  4064  trin  4138  triun  4141  truni  4142  trint  4143  iinexgm  4184  class2seteq  4193  pwuni  4222  exmid1dc  4230  exmidn0m  4231  exmidsssn  4232  exmid0el  4234  exmidel  4235  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  mss  4256  copsex2t  4275  euotd  4284  pwunim  4318  ispod  4336  sotricim  4355  exse  4368  frind  4384  trssord  4412  suctr  4453  pwnex  4481  eusvnf  4485  eusvnfb  4486  eusv2nf  4488  rexxfrd  4495  ralxfr2d  4496  rexxfr2d  4497  rabxfrd  4501  reuhypd  4503  eldifpw  4509  iunpw  4512  ssorduni  4520  onsucb  4536  onsucelsucr  4541  sucunielr  4543  ontriexmidim  4555  ordtri2or2exmidlem  4559  onsucelsucexmid  4563  reg2exmidlema  4567  setindel  4571  elirr  4574  orddisj  4579  en2lp  4587  suc11g  4590  ordsuc  4596  nlimsucg  4599  ordtri2or2exmid  4604  ontri2orexmidim  4605  zfregfr  4607  wessep  4611  tfi  4615  peano5  4631  limom  4647  peano2b  4648  nndceq0  4651  nnpredcl  4656  0nelrel  4706  eqrelrdv  4756  xpsspw  4772  relint  4784  relop  4813  eqbrrdva  4833  opeldm  4866  elres  4979  relssres  4981  elrelimasn  5032  exse2  5040  issref  5049  trin2  5058  dminss  5081  imainss  5082  rnxpid  5101  dmsn0el  5136  dmmptg  5164  relrelss  5193  cnviinm  5208  iotanul  5231  sniota  5246  dffun5r  5267  funmo  5270  funco  5295  funun  5299  funprg  5305  funtpg  5306  funtp  5308  fntpg  5311  fununi  5323  funcnvuni  5324  imadiflem  5334  imainlem  5336  funimaexglem  5338  isarep2  5342  fnunsn  5362  2elresin  5366  fnimadisj  5375  dmmptd  5385  fco  5420  funssxp  5424  fssres  5430  feu  5437  fimacnvdisj  5439  fabexg  5442  f00  5446  f0rn0  5449  f1co  5472  fores  5487  foco  5488  f1ores  5516  foimacnv  5519  f1oun  5521  fun11iun  5522  f1oco  5524  fo00  5537  brprcneu  5548  fv3  5578  relelfvdm  5587  nfvres  5589  nfunsn  5590  funfvbrb  5672  respreima  5687  dff2  5703  dff3im  5704  dffo4  5707  fvmptelcdm  5712  ffvresb  5722  f1oresrab  5724  fmptco  5725  fsn  5731  fpr  5741  ftpg  5743  fsnunf  5759  fsnunfv  5760  elabrex  5801  dff1o6  5820  foeqcnvco  5834  fliftel1  5838  isores1  5858  isoini2  5863  riotasbc  5890  acexmidlemph  5912  acexmidlemcase  5914  oprabidlem  5950  brabvv  5965  eloprabga  6006  fnoprabg  6020  caovimo  6114  oprabexd  6181  uchoice  6192  fo1stresm  6216  fo2ndresm  6217  unielxp  6229  1st2ndbr  6239  fmpoco  6271  1stconst  6276  2ndconst  6277  poxp  6287  spc2ed  6288  disjxp1  6291  reldmtpos  6308  tposfun  6315  dftpos4  6318  smores  6347  smores2  6349  tfrlem1  6363  tfr0dm  6377  tfrlemibxssdm  6382  tfrlemibex  6384  tfrlemiubacc  6385  tfrlemi14d  6388  tfrexlem  6389  tfri1d  6390  tfr1onlembxssdm  6398  tfr1onlembex  6400  tfr1onlemubacc  6401  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllembxssdm  6411  tfrcllembex  6413  tfrcllemubacc  6414  tfrcllemres  6417  tfri3  6422  rdgon  6441  frecabcl  6454  frecfcllem  6459  frecrdg  6463  2oconcl  6494  nnsucelsuc  6546  nntri3or  6548  nndceq  6554  nndcel  6555  dcdifsnid  6559  ecexr  6594  brdifun  6616  ecelqsdm  6661  iinerm  6663  eroveu  6682  erovlem  6683  ecopovtrn  6688  ecopovtrng  6691  th3qlem1  6693  pmsspw  6739  map0b  6743  mapsn  6746  mapsncnv  6751  ixpf  6776  uniixp  6777  ixpexgg  6778  resixp  6789  f1oen3g  6810  ssdomg  6834  domtr  6841  snfig  6870  enpr2d  6873  xpf1o  6902  xpmapenlem  6907  php5dom  6921  fidceq  6927  nnfi  6930  fiunsnnn  6939  findcard  6946  findcard2  6947  findcard2s  6948  ac6sfi  6956  tridc  6957  fimax2gtri  6959  finexdc  6960  exmidpw  6966  exmidpweq  6967  exmidpw2en  6970  nnwetri  6974  unsnfi  6977  unsnfidcex  6978  unsnfidcel  6979  undifdcss  6981  tpfidisj  6986  iunfidisj  7007  snexxph  7011  fidcenumlemrks  7014  sbthlem2  7019  sbthlemi3  7020  sbthlem7  7024  sbthlemi8  7025  fival  7031  dcfi  7042  supmoti  7054  djuss  7131  updjudhf  7140  updjud  7143  casefun  7146  caseinj  7150  omp1eomlem  7155  djufun  7165  djuinj  7167  ctssdccl  7172  ctfoex  7179  nnnninf  7187  nnnninfeq2  7190  nninfisollem0  7191  nninfisollemne  7192  nninfisollemeq  7193  nninfisol  7194  finomni  7201  exmidomniim  7202  exmidomni  7203  fodjuomnilemdc  7205  omniwomnimkv  7228  nninfdcinf  7232  nninfwlporlem  7234  nninfwlpoimlemg  7236  nninfwlpoim  7239  exmidonfinlem  7255  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  dju1en  7275  exmidontriimlem1  7283  exmidontriimlem3  7285  pw1on  7288  3nsssucpw1  7298  2omotaplemap  7319  2omotap  7321  exmidmotap  7323  cc4f  7331  cc4n  7333  dmaddpqlem  7439  nqpi  7440  dmaddpq  7441  dmmulpq  7442  ltdcnq  7459  subhalfnqq  7476  enq0sym  7494  enq0ref  7495  enq0tr  7496  nqnq0pi  7500  nq0nn  7504  addnq0mo  7509  mulnq0mo  7510  nqpnq0nq  7515  nqnq0a  7516  nqnq0m  7517  npsspw  7533  elnp1st2nd  7538  prnmaxl  7550  prnminu  7551  prarloc  7565  genprndl  7583  genprndu  7584  nqprm  7604  nqprl  7613  nqpru  7614  addnqprlemrl  7619  addnqprlemru  7620  prmuloc  7628  mulnqprlemrl  7635  mulnqprlemru  7636  ltsopr  7658  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  lteupri  7679  recexprlemopl  7687  recexprlemopu  7689  recexprlemdisj  7692  archpr  7705  cauappcvgprlemdisj  7713  cauappcvgprlemladdrl  7719  cauappcvgprlem2  7722  caucvgprlemnbj  7729  caucvgprlemdisj  7736  caucvgprlemladdfu  7739  caucvgprlem2  7742  caucvgprprlemnbj  7755  caucvgprprlemdisj  7764  suplocexprlemml  7778  suplocexprlemrl  7779  suplocexprlemmu  7780  suplocexprlemloc  7783  addsrmo  7805  mulsrmo  7806  recexgt0sr  7835  prsrpos  7847  caucvgsrlemasr  7852  suplocsrlemb  7868  suplocsrlempr  7869  suplocsr  7871  elrealeu  7891  pitonn  7910  pitoregt0  7911  pitore  7912  recnnre  7913  axaddcl  7926  axaddrcl  7927  axmulcl  7928  axmulrcl  7929  axrnegex  7941  axcnre  7943  axpre-lttrn  7946  rereceu  7951  axarch  7953  axpre-suploclemres  7963  axpre-suploc  7964  ltxrlt  8087  apirr  8626  divmulasscomap  8717  rerecclap  8751  lbreu  8966  arch  9240  0mnnnnn0  9275  nnm1nn0  9284  elnnnn0c  9288  elnnz1  9343  ztri3or0  9362  nzadd  9372  nn0n0n1ge2  9390  zdceq  9395  zdcle  9396  zdclt  9397  uzind  9431  eluzge3nn  9640  supinfneg  9663  infsupneg  9664  eluz2b2  9671  elnn1uz2  9675  elnn0dc  9679  elnndc  9680  nn01to3  9685  znq  9692  qaddcl  9703  qmulcl  9705  qreccl  9710  irradd  9714  irrmul  9715  elpq  9717  cnref1o  9719  xnn0dcle  9871  xrpnfdc  9911  xrmnfdc  9912  xaddcom  9930  xnegdi  9937  xpncan  9940  xleadd1a  9942  iooidg  9978  elioo4g  10003  elfzd  10085  fzdcel  10109  fznlem  10110  fzpreddisj  10140  fz0to4untppr  10193  elfz0ubfz0  10194  elfz0fzfz0  10195  fz0fzelfz0  10196  fz0fzdiffz0  10199  elfzmlbp  10201  difelfzle  10203  4fvwrd4  10209  fzosplit  10247  elfzo0  10252  fzo1fzo0n0  10253  elfzonn0  10256  fzofzim  10258  elfzo1  10260  elfzom1elp1fzo  10272  fzossfzop1  10282  ssfzo12bi  10295  exfzdc  10310  qdceq  10317  qdclt  10318  exbtwnzlemstep  10319  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnxr  10329  modfzo0difsn  10469  frec2uzrand  10479  frec2uzf1od  10480  frecuzrdgrcl  10484  frecuzrdgtcl  10486  frecuzrdgrclt  10489  frecuzrdgfunlem  10493  frecfzennn  10500  nninfinf  10517  seq3f1olemp  10589  seq3f1oleml  10590  seqf1oglem1  10593  ser0f  10608  expcl2lemap  10625  hashunsng  10881  iswrdinn0  10922  snopiswrd  10927  wrdlndm  10934  iswrdsymb  10935  wrdsymb1  10953  shftfvalg  10965  shftfval  10968  caucvgre  11128  rexanuz  11135  recvguniq  11142  rennim  11149  resqrexlemf  11154  rsqrmo  11174  fimaxre2  11373  climeu  11442  sumdc  11504  summodc  11529  zsumdc  11530  isum  11531  fisumss  11538  isumss2  11539  fsumsplit  11553  sumsnf  11555  fsumsplitsn  11556  sumtp  11560  sumsplitdc  11578  fsum2dlemstep  11580  fisum0diag2  11593  fsumconst  11600  modfsummodlemstep  11603  fsum00  11608  fsumabs  11611  fsumiun  11623  isumlessdc  11642  expcnv  11650  prodmodc  11724  zproddc  11725  iprodap  11726  iprodap0  11728  fprodssdc  11736  prodsnf  11738  fprodsplitdc  11742  fprodsplit  11743  fprodm1  11744  fprod1p  11745  fprodunsn  11750  fprod2dlemstep  11768  fprodsplitsn  11779  ef0lem  11806  modmulconst  11969  dvdsdivcl  11995  dvdsssfz1  11997  dvdsfac  12005  zeoxor  12013  nn0ehalf  12047  nn0oddm1d2  12053  nnoddm1d2  12054  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemstep  12085  infssuzex  12089  gcdsupex  12097  gcdsupcl  12098  bezoutlemnewy  12136  bezoutlemmain  12138  bezoutlemeu  12147  dfgcd2  12154  nnwosdc  12179  nninfct  12181  algrf  12186  algcvgblem  12190  lcmgcdlem  12218  lcmdvds  12220  coprmgcdb  12229  mulgcddvds  12235  qredeu  12238  cncongr1  12244  cncongr2  12245  isprm2lem  12257  dvdsnprmd  12266  prmdc  12271  oddprmge3  12276  pw2dvdseu  12309  phibndlem  12357  dfphi2  12361  hashdvds  12362  phiprmpw  12363  eulerthlemh  12372  hashgcdeq  12380  phisum  12381  odzdvds  12386  reumodprminv  12394  nnnn0modprm0  12396  prm23ge5  12405  pclemdc  12429  pcdvdsb  12461  difsqpwdvds  12479  oddprmdvds  12495  1arith  12508  4sqlem3  12531  4sqlemafi  12536  4sqlemffi  12537  4sqleminfi  12538  4sqexercise1  12539  4sqlem11  12542  4sqlem19  12550  ennnfonelemdc  12559  ennnfonelemh  12564  ennnfonelemhf1o  12573  ennnfonelemf1  12578  ennnfonelemrn  12579  ennnfonelemdm  12580  exmidunben  12586  ctinfomlemom  12587  ctinfom  12588  ctiunctlemudc  12597  ctiunctlemf  12598  ctiunctal  12601  nninfdclemcl  12608  nninfdclemf  12609  nninfdclemp1  12610  isstructim  12635  setsresg  12659  strleund  12724  1strbas  12738  2strbasg  12740  2stropg  12741  restsspw  12863  tgval  12876  ptex  12878  imasaddfnlemg  12900  fnpr2o  12925  fnpr2ob  12926  mgmidsssn0  12970  fngsum  12974  igsumvalx  12975  isnsgrp  12992  sgrpidmndm  13004  mndinvmod  13029  mnd1  13030  mhmeql  13067  grpinveu  13113  mulgval  13195  subgintm  13271  trivsubgsnd  13274  eqgfval  13295  ecqusaddd  13311  ecqusaddcl  13312  ghmeql  13340  iscmnd  13371  imasabl  13409  gsumfzmhm2  13417  rnglz  13444  srgfcl  13472  reldvdsrsrg  13591  rhmopp  13675  subrgdvds  13734  lssuni  13862  lssintclm  13883  lspf  13888  qusmulrng  14031  mulgrhm2  14109  znf1o  14150  istopon  14192  toponcom  14206  topgele  14208  topontopn  14216  tsettps  14217  eltg2b  14233  unitg  14241  tgss2  14258  bastop2  14263  distop  14264  epttop  14269  cldss2  14285  neisspw  14327  neipsm  14333  neiuni  14340  tgcn  14387  tgcnp  14388  cnntr  14404  lmff  14428  txuni2  14435  txbasex  14436  txbas  14437  txcnp  14450  txcnmpt  14452  txcn  14454  txdis  14456  txdis1cn  14457  cnmpt11  14462  cnmpt12  14466  cnmpt21  14470  cnmpt2t  14472  cnmpt22  14473  blsscls2  14672  xmetxpbl  14687  xmettxlem  14688  tgqioo  14734  fsumcncntop  14746  cncfmpt1f  14777  mulcncflem  14786  mulcncf  14787  dedekindeu  14802  dedekindicclemicc  14811  dedekindicc  14812  ivthinclemdisj  14819  hovercncf  14825  limcimo  14844  cnmptlimc  14853  reldvg  14858  dvfvalap  14860  dvfgg  14867  dvmptfsum  14904  dveflem  14905  dvef  14906  elply2  14914  sincn  14945  coscn  14946  reeff1o  14949  pilem3  14959  ioocosf1o  15030  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem4  15221  lgseisenlem2  15228  lgseisenlem3  15229  lgsquadlem2  15235  2lgslem3  15258  2sqlem2  15272  mul2sq  15273  2sqlem3  15274  2sqlem7  15278  bj-trst  15301  bj-fast  15303  bj-stand  15310  bj-trdc  15314  bj-fadc  15316  decidr  15358  djulclALT  15363  djurclALT  15364  bj-charfunr  15372  bj-indind  15494  bj-2inf  15500  bj-nntrans2  15514  bj-peano4  15517  bj-nnord  15520  bj-inf2vn  15536  bj-inf2vn2  15537  bj-findis  15541  pwf1oexmid  15560  subctctexmid  15561  nnsf  15565  nninfsellemdc  15570  nninffeq  15580  nnnninfen  15581  exmidsbthrlem  15582  sbthom  15586  triap  15589  trilpo  15603  apdifflemr  15607  redcwlpo  15615  tridceq  15616  nconstwlpolem0  15623  nconstwlpolem  15625  nconstwlpo  15626  neapmkv  15628  ltlenmkv  15630