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  2850  spc2gv  2851  spc3egv  2852  spc3gv  2853  rspce  2859  ceqex  2887  elrab3t  2915  elrabd  2918  mosubt  2937  mo2icl  2939  reu3  2950  reu6i  2951  2rmorex  2966  sbc5  3009  rspesbca  3070  rmo2ilem  3075  sbnfc2  3141  ssrd  3184  ssrdv  3185  3sstr4g  3222  eqsstrid  3225  ss2abdv  3252  abssdv  3253  rabssdv  3259  ss2rabdv  3260  ssun1  3322  unssad  3336  unssbd  3337  ssddif  3393  uneqin  3410  indifdir  3415  undif3ss  3420  reuss2  3439  n0rf  3459  reximdva0m  3462  rabxmdc  3478  ssindif0im  3506  minel  3508  ralidm  3547  ralm  3550  dcun  3556  ifmdc  3597  disjsn2  3681  absneu  3690  rabsneu  3691  opprc  3825  elunii  3840  dfnfc2  3853  uniss2  3866  unidif  3867  ssunieq  3868  intab  3899  iunss2  3957  iunssd  3958  iunxdif2  3961  invdisj  4023  disjiun  4024  3brtr4g  4063  trin  4137  triun  4140  truni  4141  trint  4142  iinexgm  4183  class2seteq  4192  pwuni  4221  exmid1dc  4229  exmidn0m  4230  exmidsssn  4231  exmid0el  4233  exmidel  4234  exmidundif  4235  exmidundifim  4236  exmid1stab  4237  mss  4255  copsex2t  4274  euotd  4283  pwunim  4317  ispod  4335  sotricim  4354  exse  4367  frind  4383  trssord  4411  suctr  4452  pwnex  4480  eusvnf  4484  eusvnfb  4485  eusv2nf  4487  rexxfrd  4494  ralxfr2d  4495  rexxfr2d  4496  rabxfrd  4500  reuhypd  4502  eldifpw  4508  iunpw  4511  ssorduni  4519  onsucb  4535  onsucelsucr  4540  sucunielr  4542  ontriexmidim  4554  ordtri2or2exmidlem  4558  onsucelsucexmid  4562  reg2exmidlema  4566  setindel  4570  elirr  4573  orddisj  4578  en2lp  4586  suc11g  4589  ordsuc  4595  nlimsucg  4598  ordtri2or2exmid  4603  ontri2orexmidim  4604  zfregfr  4606  wessep  4610  tfi  4614  peano5  4630  limom  4646  peano2b  4647  nndceq0  4650  nnpredcl  4655  0nelrel  4705  eqrelrdv  4755  xpsspw  4771  relint  4783  relop  4812  eqbrrdva  4832  opeldm  4865  elres  4978  relssres  4980  elrelimasn  5031  exse2  5039  issref  5048  trin2  5057  dminss  5080  imainss  5081  rnxpid  5100  dmsn0el  5135  dmmptg  5163  relrelss  5192  cnviinm  5207  iotanul  5230  sniota  5245  dffun5r  5266  funmo  5269  funco  5294  funun  5298  funprg  5304  funtpg  5305  funtp  5307  fntpg  5310  fununi  5322  funcnvuni  5323  imadiflem  5333  imainlem  5335  funimaexglem  5337  isarep2  5341  fnunsn  5361  2elresin  5365  fnimadisj  5374  dmmptd  5384  fco  5419  funssxp  5423  fssres  5429  feu  5436  fimacnvdisj  5438  fabexg  5441  f00  5445  f0rn0  5448  f1co  5471  fores  5486  foco  5487  f1ores  5515  foimacnv  5518  f1oun  5520  fun11iun  5521  f1oco  5523  fo00  5536  brprcneu  5547  fv3  5577  relelfvdm  5586  nfvres  5588  nfunsn  5589  funfvbrb  5671  respreima  5686  dff2  5702  dff3im  5703  dffo4  5706  fvmptelcdm  5711  ffvresb  5721  f1oresrab  5723  fmptco  5724  fsn  5730  fpr  5740  ftpg  5742  fsnunf  5758  fsnunfv  5759  elabrex  5800  dff1o6  5819  foeqcnvco  5833  fliftel1  5837  isores1  5857  isoini2  5862  riotasbc  5889  acexmidlemph  5911  acexmidlemcase  5913  oprabidlem  5949  brabvv  5964  eloprabga  6005  fnoprabg  6019  caovimo  6112  oprabexd  6179  uchoice  6190  fo1stresm  6214  fo2ndresm  6215  unielxp  6227  1st2ndbr  6237  fmpoco  6269  1stconst  6274  2ndconst  6275  poxp  6285  spc2ed  6286  disjxp1  6289  reldmtpos  6306  tposfun  6313  dftpos4  6316  smores  6345  smores2  6347  tfrlem1  6361  tfr0dm  6375  tfrlemibxssdm  6380  tfrlemibex  6382  tfrlemiubacc  6383  tfrlemi14d  6386  tfrexlem  6387  tfri1d  6388  tfr1onlembxssdm  6396  tfr1onlembex  6398  tfr1onlemubacc  6399  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllembxssdm  6409  tfrcllembex  6411  tfrcllemubacc  6412  tfrcllemres  6415  tfri3  6420  rdgon  6439  frecabcl  6452  frecfcllem  6457  frecrdg  6461  2oconcl  6492  nnsucelsuc  6544  nntri3or  6546  nndceq  6552  nndcel  6553  dcdifsnid  6557  ecexr  6592  brdifun  6614  ecelqsdm  6659  iinerm  6661  eroveu  6680  erovlem  6681  ecopovtrn  6686  ecopovtrng  6689  th3qlem1  6691  pmsspw  6737  map0b  6741  mapsn  6744  mapsncnv  6749  ixpf  6774  uniixp  6775  ixpexgg  6776  resixp  6787  f1oen3g  6808  ssdomg  6832  domtr  6839  snfig  6868  enpr2d  6871  xpf1o  6900  xpmapenlem  6905  php5dom  6919  fidceq  6925  nnfi  6928  fiunsnnn  6937  findcard  6944  findcard2  6945  findcard2s  6946  ac6sfi  6954  tridc  6955  fimax2gtri  6957  finexdc  6958  exmidpw  6964  exmidpweq  6965  exmidpw2en  6968  nnwetri  6972  unsnfi  6975  unsnfidcex  6976  unsnfidcel  6977  undifdcss  6979  tpfidisj  6984  iunfidisj  7005  snexxph  7009  fidcenumlemrks  7012  sbthlem2  7017  sbthlemi3  7018  sbthlem7  7022  sbthlemi8  7023  fival  7029  dcfi  7040  supmoti  7052  djuss  7129  updjudhf  7138  updjud  7141  casefun  7144  caseinj  7148  omp1eomlem  7153  djufun  7163  djuinj  7165  ctssdccl  7170  ctfoex  7177  nnnninf  7185  nnnninfeq2  7188  nninfisollem0  7189  nninfisollemne  7190  nninfisollemeq  7191  nninfisol  7192  finomni  7199  exmidomniim  7200  exmidomni  7201  fodjuomnilemdc  7203  omniwomnimkv  7226  nninfdcinf  7230  nninfwlporlem  7232  nninfwlpoimlemg  7234  nninfwlpoim  7237  exmidonfinlem  7253  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  dju1en  7273  exmidontriimlem1  7281  exmidontriimlem3  7283  pw1on  7286  3nsssucpw1  7296  2omotaplemap  7317  2omotap  7319  exmidmotap  7321  cc4f  7329  cc4n  7331  dmaddpqlem  7437  nqpi  7438  dmaddpq  7439  dmmulpq  7440  ltdcnq  7457  subhalfnqq  7474  enq0sym  7492  enq0ref  7493  enq0tr  7494  nqnq0pi  7498  nq0nn  7502  addnq0mo  7507  mulnq0mo  7508  nqpnq0nq  7513  nqnq0a  7514  nqnq0m  7515  npsspw  7531  elnp1st2nd  7536  prnmaxl  7548  prnminu  7549  prarloc  7563  genprndl  7581  genprndu  7582  nqprm  7602  nqprl  7611  nqpru  7612  addnqprlemrl  7617  addnqprlemru  7618  prmuloc  7626  mulnqprlemrl  7633  mulnqprlemru  7634  ltsopr  7656  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  lteupri  7677  recexprlemopl  7685  recexprlemopu  7687  recexprlemdisj  7690  archpr  7703  cauappcvgprlemdisj  7711  cauappcvgprlemladdrl  7717  cauappcvgprlem2  7720  caucvgprlemnbj  7727  caucvgprlemdisj  7734  caucvgprlemladdfu  7737  caucvgprlem2  7740  caucvgprprlemnbj  7753  caucvgprprlemdisj  7762  suplocexprlemml  7776  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemloc  7781  addsrmo  7803  mulsrmo  7804  recexgt0sr  7833  prsrpos  7845  caucvgsrlemasr  7850  suplocsrlemb  7866  suplocsrlempr  7867  suplocsr  7869  elrealeu  7889  pitonn  7908  pitoregt0  7909  pitore  7910  recnnre  7911  axaddcl  7924  axaddrcl  7925  axmulcl  7926  axmulrcl  7927  axrnegex  7939  axcnre  7941  axpre-lttrn  7944  rereceu  7949  axarch  7951  axpre-suploclemres  7961  axpre-suploc  7962  ltxrlt  8085  apirr  8624  divmulasscomap  8715  rerecclap  8749  lbreu  8964  arch  9237  0mnnnnn0  9272  nnm1nn0  9281  elnnnn0c  9285  elnnz1  9340  ztri3or0  9359  nzadd  9369  nn0n0n1ge2  9387  zdceq  9392  zdcle  9393  zdclt  9394  uzind  9428  eluzge3nn  9637  supinfneg  9660  infsupneg  9661  eluz2b2  9668  elnn1uz2  9672  elnn0dc  9676  elnndc  9677  nn01to3  9682  znq  9689  qaddcl  9700  qmulcl  9702  qreccl  9707  irradd  9711  irrmul  9712  elpq  9714  cnref1o  9716  xnn0dcle  9868  xrpnfdc  9908  xrmnfdc  9909  xaddcom  9927  xnegdi  9934  xpncan  9937  xleadd1a  9939  iooidg  9975  elioo4g  10000  elfzd  10082  fzdcel  10106  fznlem  10107  fzpreddisj  10137  fz0to4untppr  10190  elfz0ubfz0  10191  elfz0fzfz0  10192  fz0fzelfz0  10193  fz0fzdiffz0  10196  elfzmlbp  10198  difelfzle  10200  4fvwrd4  10206  fzosplit  10244  elfzo0  10249  fzo1fzo0n0  10250  elfzonn0  10253  fzofzim  10255  elfzo1  10257  elfzom1elp1fzo  10269  fzossfzop1  10279  ssfzo12bi  10292  exfzdc  10307  qdceq  10314  qdclt  10315  exbtwnzlemstep  10316  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnxr  10326  modfzo0difsn  10466  frec2uzrand  10476  frec2uzf1od  10477  frecuzrdgrcl  10481  frecuzrdgtcl  10483  frecuzrdgrclt  10486  frecuzrdgfunlem  10490  frecfzennn  10497  nninfinf  10514  seq3f1olemp  10586  seq3f1oleml  10587  seqf1oglem1  10590  ser0f  10605  expcl2lemap  10622  hashunsng  10878  iswrdinn0  10919  snopiswrd  10924  wrdlndm  10931  iswrdsymb  10932  wrdsymb1  10950  shftfvalg  10962  shftfval  10965  caucvgre  11125  rexanuz  11132  recvguniq  11139  rennim  11146  resqrexlemf  11151  rsqrmo  11171  fimaxre2  11370  climeu  11439  sumdc  11501  summodc  11526  zsumdc  11527  isum  11528  fisumss  11535  isumss2  11536  fsumsplit  11550  sumsnf  11552  fsumsplitsn  11553  sumtp  11557  sumsplitdc  11575  fsum2dlemstep  11577  fisum0diag2  11590  fsumconst  11597  modfsummodlemstep  11600  fsum00  11605  fsumabs  11608  fsumiun  11620  isumlessdc  11639  expcnv  11647  prodmodc  11721  zproddc  11722  iprodap  11723  iprodap0  11725  fprodssdc  11733  prodsnf  11735  fprodsplitdc  11739  fprodsplit  11740  fprodm1  11741  fprod1p  11742  fprodunsn  11747  fprod2dlemstep  11765  fprodsplitsn  11776  ef0lem  11803  modmulconst  11966  dvdsdivcl  11992  dvdsssfz1  11994  dvdsfac  12002  zeoxor  12010  nn0ehalf  12044  nn0oddm1d2  12050  nnoddm1d2  12051  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemstep  12082  infssuzex  12086  gcdsupex  12094  gcdsupcl  12095  bezoutlemnewy  12133  bezoutlemmain  12135  bezoutlemeu  12144  dfgcd2  12151  nnwosdc  12176  nninfct  12178  algrf  12183  algcvgblem  12187  lcmgcdlem  12215  lcmdvds  12217  coprmgcdb  12226  mulgcddvds  12232  qredeu  12235  cncongr1  12241  cncongr2  12242  isprm2lem  12254  dvdsnprmd  12263  prmdc  12268  oddprmge3  12273  pw2dvdseu  12306  phibndlem  12354  dfphi2  12358  hashdvds  12359  phiprmpw  12360  eulerthlemh  12369  hashgcdeq  12377  phisum  12378  odzdvds  12383  reumodprminv  12391  nnnn0modprm0  12393  prm23ge5  12402  pclemdc  12426  pcdvdsb  12458  difsqpwdvds  12476  oddprmdvds  12492  1arith  12505  4sqlem3  12528  4sqlemafi  12533  4sqlemffi  12534  4sqleminfi  12535  4sqexercise1  12536  4sqlem11  12539  4sqlem19  12547  ennnfonelemdc  12556  ennnfonelemh  12561  ennnfonelemhf1o  12570  ennnfonelemf1  12575  ennnfonelemrn  12576  ennnfonelemdm  12577  exmidunben  12583  ctinfomlemom  12584  ctinfom  12585  ctiunctlemudc  12594  ctiunctlemf  12595  ctiunctal  12598  nninfdclemcl  12605  nninfdclemf  12606  nninfdclemp1  12607  isstructim  12632  setsresg  12656  strleund  12721  1strbas  12735  2strbasg  12737  2stropg  12738  restsspw  12860  tgval  12873  ptex  12875  imasaddfnlemg  12897  fnpr2o  12922  fnpr2ob  12923  mgmidsssn0  12967  fngsum  12971  igsumvalx  12972  isnsgrp  12989  sgrpidmndm  13001  mndinvmod  13026  mnd1  13027  mhmeql  13064  grpinveu  13110  mulgval  13192  subgintm  13268  trivsubgsnd  13271  eqgfval  13292  ecqusaddd  13308  ecqusaddcl  13309  ghmeql  13337  iscmnd  13368  imasabl  13406  gsumfzmhm2  13414  rnglz  13441  srgfcl  13469  reldvdsrsrg  13588  rhmopp  13672  subrgdvds  13731  lssuni  13859  lssintclm  13880  lspf  13885  qusmulrng  14028  mulgrhm2  14098  znf1o  14139  istopon  14181  toponcom  14195  topgele  14197  topontopn  14205  tsettps  14206  eltg2b  14222  unitg  14230  tgss2  14247  bastop2  14252  distop  14253  epttop  14258  cldss2  14274  neisspw  14316  neipsm  14322  neiuni  14329  tgcn  14376  tgcnp  14377  cnntr  14393  lmff  14417  txuni2  14424  txbasex  14425  txbas  14426  txcnp  14439  txcnmpt  14441  txcn  14443  txdis  14445  txdis1cn  14446  cnmpt11  14451  cnmpt12  14455  cnmpt21  14459  cnmpt2t  14461  cnmpt22  14462  blsscls2  14661  xmetxpbl  14676  xmettxlem  14677  tgqioo  14715  fsumcncntop  14724  cncfmpt1f  14752  mulcncflem  14761  mulcncf  14762  dedekindeu  14777  dedekindicclemicc  14786  dedekindicc  14787  ivthinclemdisj  14794  hovercncf  14800  limcimo  14819  cnmptlimc  14828  reldvg  14833  dvfvalap  14835  dvfgg  14842  dveflem  14872  dvef  14873  elply2  14881  sincn  14904  coscn  14905  reeff1o  14908  pilem3  14918  ioocosf1o  14989  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem4  15180  lgseisenlem2  15187  lgseisenlem3  15188  2sqlem2  15202  mul2sq  15203  2sqlem3  15204  2sqlem7  15208  bj-trst  15231  bj-fast  15233  bj-stand  15240  bj-trdc  15244  bj-fadc  15246  decidr  15288  djulclALT  15293  djurclALT  15294  bj-charfunr  15302  bj-indind  15424  bj-2inf  15430  bj-nntrans2  15444  bj-peano4  15447  bj-nnord  15450  bj-inf2vn  15466  bj-inf2vn2  15467  bj-findis  15471  pwf1oexmid  15490  subctctexmid  15491  nnsf  15495  nninfsellemdc  15500  nninffeq  15510  nnnninfen  15511  exmidsbthrlem  15512  sbthom  15516  triap  15519  trilpo  15533  apdifflemr  15537  redcwlpo  15545  tridceq  15546  nconstwlpolem0  15553  nconstwlpolem  15555  nconstwlpo  15556  neapmkv  15558  ltlenmkv  15560