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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbbr  136  pm5.74rd  183  bitri  184  3imtr4i  201  sylanbrc  421  mpnanrd  704  oibabs  726  dcim  853  dcstab  856  stdcndc  857  stdcndcOLD  858  dcand  945  dcor  948  dfifp2dc  994  3mix1  1197  3mix2  1198  3jca  1208  syl3anbrc  1212  syl21anbrc  1213  inegd  1421  pclem6  1423  xoranor  1426  dcfrompeirce  1499  nfxfrd  1528  nfd  1576  hban  1600  nfan1  1617  nford  1620  nfand  1621  hbim1  1623  nfal  1629  alexim  1698  nnal  1702  hbn  1703  nf4r  1723  19.34  1736  nfexd  1814  sbcof2  1863  nfsb2or  1890  sbidm  1904  nfdv  1930  nfd2  2082  nfeudv  2101  mon  2115  eumo  2118  mo23  2128  eu2  2131  eu3h  2132  exmodc  2137  exmonim  2138  mo2r  2139  mo3h  2140  bm1.1  2223  eqrdv  2236  3eltr4g  2324  abbi2dv  2359  abbi1dv  2360  nfcd  2387  nfcxfrd  2390  dcned  2426  neqned  2427  3netr4g  2455  necon3bi  2470  necon2ai  2474  nnral  2540  alral  2595  rspe  2599  rsp2e  2601  rgen2a  2604  ralrimi  2621  r19.27v  2678  r19.28v  2679  r19.27av  2686  r19.32r  2697  nfreudxy  2725  mormo  2769  nrexrmo  2774  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  rspce  2924  ceqex  2953  elrab3t  2981  elrabd  2984  mosubt  3003  mo2icl  3005  reu3  3016  reu6i  3017  2rmorex  3032  sbc5  3075  rspesbca  3137  rmo2ilem  3142  sbnfc2  3208  ssrd  3253  ssrdv  3254  3sstr4g  3291  eqsstrid  3294  ss2abdv  3321  abssdv  3322  rabssdv  3328  ss2rabdv  3329  ssun1  3392  unssad  3406  unssbd  3407  ssddif  3465  uneqin  3482  indifdir  3487  undif3ss  3492  reuss2  3513  n0rf  3534  reximdva0m  3537  rabxmdc  3554  ssindif0im  3584  minel  3586  ralidm  3628  ralm  3631  dcun  3637  ifmdc  3683  ifeqeqxdc  3687  disjsn2  3772  rabsnif  3778  absneu  3783  rabsneu  3784  opprc  3925  elunii  3940  dfnfc2  3953  uniss2  3966  unidif  3967  ssunieq  3968  intab  3999  iunss2  4057  iunssd  4058  iunxdif2  4061  invdisj  4123  disjiun  4125  3brtr4g  4164  trin  4239  triun  4242  truni  4243  trint  4244  iinexgm  4290  class2seteq  4300  pwuni  4329  exmid1dc  4337  exmidn0m  4338  exmidsssn  4339  exmid0el  4341  exmidel  4342  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  mss  4366  copsex2t  4385  euotd  4395  pwunim  4431  ispod  4449  sotricim  4468  exse  4481  frind  4497  trssord  4525  suctr  4566  pwnex  4595  eusvnf  4599  eusvnfb  4600  eusv2nf  4602  rexxfrd  4609  ralxfr2d  4610  rexxfr2d  4611  rabxfrd  4615  reuhypd  4617  eldifpw  4623  iunpw  4626  ssorduni  4634  onsucb  4650  onsucelsucr  4655  sucunielr  4657  ontriexmidim  4669  ordtri2or2exmidlem  4673  onsucelsucexmid  4677  reg2exmidlema  4681  setindel  4685  elirr  4688  orddisj  4693  en2lp  4701  suc11g  4704  ordsuc  4710  nlimsucg  4713  ordtri2or2exmid  4718  ontri2orexmidim  4719  zfregfr  4721  wessep  4725  tfi  4729  peano5  4745  limom  4761  peano2b  4762  nndceq0  4765  nnpredcl  4770  0nelrel  4821  eqrelrdv  4871  xpsspw  4887  relint  4901  relop  4930  eqbrrdva  4950  ssrelrn  4972  opeldm  4984  reldmm  5000  elres  5099  relssres  5101  elrelimasn  5153  exse2  5161  issref  5170  trin2  5179  dminss  5202  imainss  5203  rnxpid  5222  dmsn0el  5257  dmmptg  5285  relrelss  5314  cnviinm  5329  iotanul  5353  sniota  5368  dffun5r  5389  funmo  5392  funco  5417  funun  5422  fununmo  5423  fununfun  5424  funprg  5431  funtpg  5432  funtp  5434  fntpg  5437  fununi  5449  funcnvuni  5450  imadiflem  5460  imainlem  5462  funimaexglem  5464  isarep2  5468  fnunsn  5490  2elresin  5494  fnimadisj  5504  dmmptd  5514  fco  5552  funssxp  5557  fssres  5565  feu  5574  fimacnvdisj  5576  fabexg  5579  f00  5584  f0rn0  5587  f1co  5610  fores  5625  foco  5626  f1ores  5654  foimacnv  5657  f1oun  5659  fun11iun  5660  f1oco  5662  fo00  5677  brprcneu  5688  fv3  5718  relelfvdm  5727  nfvres  5732  nfunsn  5733  funfvbrb  5822  respreima  5836  dff2  5852  dff3im  5853  dffo4  5856  fvmptelcdm  5861  ffvresb  5871  f1oresrab  5873  fmptco  5874  fsn  5880  fcof  5894  fpr  5897  ftpg  5899  fsnunf  5915  fsnunfv  5916  elabrex  5963  dff1o6  5982  foeqcnvco  5996  fliftel1  6000  isores1  6020  isoini2  6025  riotasbc  6055  acexmidlemph  6078  acexmidlemcase  6080  oprabidlem  6116  brabvv  6134  eloprabga  6175  fnoprabg  6189  caovimo  6283  oprabexd  6360  uchoice  6371  fo1stresm  6395  fo2ndresm  6396  unielxp  6408  1st2ndbr  6418  opabn1stprc  6429  fmpoco  6452  1stconst  6457  2ndconst  6458  poxp  6468  spc2ed  6469  disjxp1  6472  elmpom  6474  suppsnopdc  6490  reldmtpos  6524  tposfun  6531  dftpos4  6534  smores  6563  smores2  6565  tfrlem1  6579  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemibex  6600  tfrlemiubacc  6601  tfrlemi14d  6604  tfrexlem  6605  tfri1d  6606  tfr1onlembxssdm  6614  tfr1onlembex  6616  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllembxssdm  6627  tfrcllembex  6629  tfrcllemubacc  6630  tfrcllemres  6633  tfri3  6638  rdgon  6657  frecabcl  6670  frecfcllem  6675  frecrdg  6679  2oconcl  6712  nnsucelsuc  6764  nntri3or  6766  nndceq  6772  nndcel  6773  dcdifsnid  6777  ecexr  6812  brdifun  6834  ecelqsdm  6879  iinerm  6881  eroveu  6900  erovlem  6901  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  fsetdmprc0  6950  pmsspw  6964  map0b  6968  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpf  7002  uniixp  7003  ixpexgg  7004  resixp  7015  f1oen3g  7040  ssdomg  7065  domtr  7072  snfig  7103  modom  7108  enpr2d  7111  dom1o  7116  xpf1o  7144  xpmapenlem  7149  php5dom  7164  fidceq  7171  nnfi  7174  fiunsnnn  7185  findcard  7192  findcard2  7193  findcard2s  7194  ac6sfi  7202  fidcen  7203  tridc  7204  fimax2gtri  7206  finexdc  7207  elssdc  7209  eqsndc  7210  exmidpw  7215  exmidpweq  7216  exmidpw2en  7219  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  tpfidisj  7236  tpfidceq  7237  exmidssfi  7246  iunfidisj  7260  mapfi  7261  fissfi  7263  snexxph  7267  fidcenumlemrks  7270  sbthlem2  7275  sbthlemi3  7276  sbthlem7  7280  sbthlemi8  7281  fival  7304  dcfi  7315  fdcf1  7316  f1setfi  7317  supmoti  7334  djuss  7411  updjudhf  7420  updjud  7423  casefun  7426  caseinj  7430  omp1eomlem  7435  djufun  7445  djuinj  7447  ctssdccl  7452  ctfoex  7459  nnnninf  7467  nnnninfeq2  7470  nninfisollem0  7471  nninfisollemne  7472  nninfisollemeq  7473  nninfisol  7474  finomni  7481  exmidomniim  7482  exmidomni  7483  fodjuomnilemdc  7485  omniwomnimkv  7508  nninfdcinf  7512  nninfwlporlem  7514  nninfwlpoimlemg  7516  nninfwlpoim  7520  nninfinfwlpo  7521  exmidonfinlem  7546  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  finacn  7561  exmidaclem  7565  dju1en  7570  exmidontriimlem1  7578  exmidontriimlem3  7580  iftrueb01  7583  pw1on  7586  3nsssucpw1  7596  2omotaplemap  7624  2omotap  7626  exmidmotap  7628  cc4f  7636  cc4n  7638  acnccim  7639  dmaddpqlem  7745  nqpi  7746  dmaddpq  7747  dmmulpq  7748  ltdcnq  7765  subhalfnqq  7782  enq0sym  7800  enq0ref  7801  enq0tr  7802  nqnq0pi  7806  nq0nn  7810  addnq0mo  7815  mulnq0mo  7816  nqpnq0nq  7821  nqnq0a  7822  nqnq0m  7823  npsspw  7839  elnp1st2nd  7844  prnmaxl  7856  prnminu  7857  prarloc  7871  genprndl  7889  genprndu  7890  nqprm  7910  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  prmuloc  7934  mulnqprlemrl  7941  mulnqprlemru  7942  ltsopr  7964  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  lteupri  7985  recexprlemopl  7993  recexprlemopu  7995  recexprlemdisj  7998  archpr  8011  cauappcvgprlemdisj  8019  cauappcvgprlemladdrl  8025  cauappcvgprlem2  8028  caucvgprlemnbj  8035  caucvgprlemdisj  8042  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemnbj  8061  caucvgprprlemdisj  8070  suplocexprlemml  8084  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemloc  8089  addsrmo  8111  mulsrmo  8112  recexgt0sr  8141  prsrpos  8153  caucvgsrlemasr  8158  suplocsrlemb  8174  suplocsrlempr  8175  suplocsr  8177  elrealeu  8197  pitonn  8216  pitoregt0  8217  pitore  8218  recnnre  8219  axaddcl  8232  axaddrcl  8233  axmulcl  8234  axmulrcl  8235  axrnegex  8247  axcnre  8249  axpre-lttrn  8252  rereceu  8257  axarch  8259  axpre-suploclemres  8269  axpre-suploc  8270  ltxrlt  8392  apirr  8936  divmulasscomap  9029  rerecclap  9063  lbreu  9278  indconst1  9306  arch  9565  0mnnnnn0  9600  nnm1nn0  9609  elnnnn0c  9613  elnnz1  9672  ztri3or0  9691  nzadd  9702  nn0n0n1ge2  9720  zdceq  9725  zdcle  9726  zdclt  9727  uzind  9762  eluzge3nn  9982  supinfneg  10005  infsupneg  10006  eluz2b2  10013  elnn1uz2  10017  elnn0dc  10021  elnndc  10022  nn01to3  10027  znq  10034  qaddcl  10045  qmulcl  10047  qreccl  10052  irradd  10056  irrmul  10058  elpq  10060  cnref1o  10062  xnn0dcle  10215  xrpnfdc  10255  xrmnfdc  10256  xaddcom  10274  xnegdi  10281  xpncan  10284  xleadd1a  10286  iooidg  10322  elioo4g  10347  elfzd  10430  fzdcel  10455  fznlem  10456  fzpreddisj  10489  fz0to4untppr  10542  elfz0ubfz0  10543  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzmlbp  10550  difelfzle  10552  4fvwrd4  10558  fzosplit  10597  elfzo0  10604  nn0p1elfzo  10605  fzo1fzo0n0  10606  elfzonn0  10609  fzofzim  10611  elfzo1  10614  elfzom1elp1fzo  10631  fzossfzop1  10641  ssfzo12bi  10654  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  qdceq  10690  qdclt  10691  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnxr  10703  modfzo0difsn  10847  frec2uzrand  10857  frec2uzf1od  10858  frecuzrdgrcl  10862  frecuzrdgtcl  10864  frecuzrdgrclt  10867  frecuzrdgfunlem  10871  frecfzennn  10878  nninfinf  10895  seq3f1olemp  10967  seq3f1oleml  10968  seqf1oglem1  10971  ser0f  10986  expcl2lemap  11003  hashunsng  11264  hashmap  11284  sshashneg  11297  hashfibclem  11298  hashfibc  11299  hashf1lem1  11301  hashf1lem2  11302  iswrdinn0  11325  snopiswrd  11330  wrdlndm  11337  iswrdsymb  11338  wrdsymb1  11357  ccatfv0  11387  ccatval21sw  11389  lswccatn0lsw  11395  eqs1  11412  ccat1st1st  11425  lswccats1fst  11428  fzowrddc  11435  swrdfv0  11442  swrdlen2  11450  swrdfv2  11451  swrdsbslen  11454  swrdspsleq  11455  pfxfv0  11480  pfxtrcfv0  11482  pfxeq  11484  pfx1  11491  swrdswrdlem  11492  cats1un  11509  pfxccatin12lem2a  11515  pfxccatin12lem2  11519  pfxccatin12lem3  11520  swrdccat  11523  cats1fvn  11552  cats1fvnd  11553  shftfvalg  11599  shftfval  11602  caucvgre  11763  rexanuz  11770  recvguniq  11777  rennim  11784  resqrexlemf  11789  rsqrmo  11809  fimaxre2  12010  climeu  12081  sumdc  12143  summodc  12169  zsumdc  12170  isum  12171  fisumss  12178  isumss2  12179  fsumsplit  12193  sumsnf  12195  fsumsplitsn  12196  sumtp  12200  sumsplitdc  12218  fsum2dlemstep  12220  fisum0diag2  12233  fsumconst  12240  modfsummodlemstep  12243  fsum00  12248  fsumabs  12251  fsumiun  12263  isumlessdc  12282  expcnv  12290  prodmodc  12364  zproddc  12365  iprodap  12366  iprodap0  12368  fprodssdc  12376  prodsnf  12378  fprodsplitdc  12382  fprodsplit  12383  fprodm1  12384  fprod1p  12385  fprodunsn  12390  fprod2dlemstep  12408  fprodsplitsn  12419  ef0lem  12446  modmulconst  12609  dvdsdivcl  12636  dvdsssfz1  12638  dvdsfac  12646  zeoxor  12655  nn0ehalf  12689  nn0oddm1d2  12695  nnoddm1d2  12696  divalglemeunn  12707  divalglemeuneg  12709  bitsfzolem  12740  bitsinv1  12748  gcdsupex  12753  gcdsupcl  12754  bezoutlemnewy  12792  bezoutlemmain  12794  bezoutlemeu  12803  dfgcd2  12810  nnwosdc  12835  nninfct  12837  algrf  12842  algcvgblem  12846  lcmgcdlem  12874  lcmdvds  12876  coprmgcdb  12885  mulgcddvds  12891  qredeu  12894  cncongr1  12900  cncongr2  12901  isprm2lem  12913  dvdsnprmd  12922  prmdc  12927  prmdcz  12928  oddprmge3  12933  pwbdvdseu  12966  nn0sqdcq  13007  phibndlem  13017  dfphi2  13021  hashdvds  13022  phiprmpw  13023  eulerthlemh  13032  hashgcdeq  13041  phisum  13042  odzdvds  13047  reumodprminv  13055  nnnn0modprm0  13057  prm23ge5  13066  pclemdc  13090  pcdvdsb  13122  difsqpwdvds  13140  oddprmdvds  13156  1arith  13169  4sqlem3  13192  4sqlemafi  13197  4sqlemffi  13198  4sqleminfi  13199  4sqexercise1  13200  4sqlem11  13203  4sqlem19  13211  ballotfilemcdc  13275  ballotfilemdifcfi  13277  ballotfilemdifcfz  13279  ballotfilem2  13280  ballotfilemiex  13296  ballotfilemscl  13299  ballotfilemth  13333  ennnfonelemdc  13342  ennnfonelemh  13347  ennnfonelemhf1o  13356  ennnfonelemf1  13361  ennnfonelemrn  13362  ennnfonelemdm  13363  exmidunben  13369  ctinfomlemom  13370  ctinfom  13371  ctiunctlemudc  13380  ctiunctlemf  13381  ctiunctal  13384  nninfdclemcl  13391  nninfdclemf  13392  nninfdclemp1  13393  isstructim  13418  setsresg  13442  strleund  13510  1strbas  13524  2strbasg  13527  2stropg  13528  restsspw  13656  tgval  13669  ptex  13671  imasaddfnlemg  13688  fnpr2o  13713  fnpr2ob  13714  mgmidsssn0  13757  fngzsum  13761  gzsumvalx  13762  isnsgrp  13774  sgrpidmndm  13786  mndinvmod  13811  mnd1  13815  mhmeql  13852  grpinveu  13896  mulgval  13978  subgintm  14054  trivsubgsnd  14057  eqgfval  14078  ecqusaddd  14094  ecqusaddcl  14095  ghmeql  14123  iscmnd  14185  imasabl  14224  gzsummhm2  14230  gsump1  14241  gsummptfidmsplit  14248  gsumsnfdcmn  14250  gsumunsnfd  14252  gsummhm2fi  14256  prdsinvlem  14287  rnglz  14335  srgfcl  14368  rhmopp  14574  opprlring  14595  subrgdvds  14634  lssuni  14791  lssintclm  14812  lspf  14817  qusmulrng  14960  mulgrhm2  15036  znf1o  15077  aspid  15108  psrbagfi  15150  psrbagconcl  15155  psr1clfi  15177  mplsubgfilemcl  15189  istopon  15213  toponcom  15227  topgele  15229  topontopn  15237  tsettps  15238  eltg2b  15254  unitg  15262  tgss2  15279  bastop2  15284  distop  15285  epttop  15290  cldss2  15306  neisspw  15348  neipsm  15354  neiuni  15361  tgcn  15408  tgcnp  15409  cnntr  15425  lmff  15449  txuni2  15456  txbasex  15457  txbas  15458  txcnp  15471  txcnmpt  15473  txcn  15475  txdis  15477  txdis1cn  15478  cnmpt11  15483  cnmpt12  15487  cnmpt21  15491  cnmpt2t  15493  cnmpt22  15494  blsscls2  15693  xmetxpbl  15708  xmettxlem  15709  tgqioo  15755  fsumcncntop  15767  cncfmpt1f  15798  mulcncflem  15807  mulcncf  15808  dedekindeu  15823  dedekindicclemicc  15832  dedekindicc  15833  ivthinclemdisj  15840  hovercncf  15846  limcimo  15865  cnmptlimc  15874  reldvg  15879  dvfvalap  15881  dvfgg  15888  dvmptfsum  15925  dveflem  15926  dvef  15927  elply2  15935  sincn  15969  coscn  15970  reeff1o  15973  pilem3  15984  ioocosf1o  16056  ppiqfi  16216  prmdvdsfi  16217  ppiprm  16233  ppinprm  16234  chtprm  16235  chtnprm  16236  chtdif  16238  efchtqdvds  16239  ppidif  16243  prmorcht  16256  mpodvdsmulf1o  16258  fsumdvdsmul  16259  ppiqub  16267  perfectlem2  16274  bcmono  16278  bpos  16294  lgsne0  16336  gausslemma2dlem1a  16356  gausslemma2dlem4  16362  lgseisenlem2  16369  lgseisenlem3  16370  lgsquadlem2  16376  2lgslem3  16399  2sqlem2  16413  mul2sq  16414  2sqlem3  16415  2sqlem7  16419  edgstruct  16484  pw0ss  16503  incistruhgr  16510  upgrex  16523  umgrnloop0  16537  upgr1een  16544  lfgrnloopen  16553  umgredg  16565  umgrnloop2  16571  uspgredgiedg  16598  uspgriedgedg  16599  usgrislfuspgrdom  16610  usgredg3  16634  uspgredg2vlem  16640  uspgredg2v  16641  ushgredgedg  16646  ushgredgedgloop  16648  uhgr0vsize0en  16655  usgr1e  16661  subusgr  16695  vtxedgfi  16709  vtxlpfi  16710  vtxdumgrfival  16718  1loopgrvd2fi  16725  p1evtxdeqfilem  16731  vdegp1aid  16734  wlkcprim  16770  wlk1walkdom  16779  uspgr2wlkeq  16785  upgr2wlkdc  16797  wlkres  16799  clwwlkccatlem  16820  clwwlknp  16837  umgr2cwwk2dif  16844  trlsegvdegfi  16887  eupth2lem3lem3fi  16890  eupth2lem3lem6fi  16891  eupth2lem3lem4fi  16893  eupth2lembfi  16897  depindlem1  16926  bj-trst  16946  bj-fast  16948  bj-stand  16955  bj-trdc  16959  bj-fadc  16961  decidr  17003  djulclALT  17008  djurclALT  17009  bj-charfunr  17015  bj-indind  17137  bj-2inf  17143  bj-nntrans2  17157  bj-peano4  17160  bj-nnord  17163  bj-inf2vn  17179  bj-inf2vn2  17180  bj-findis  17184  pwf1oexmid  17208  subctctexmid  17209  pw1dceq  17214  exmidnotnotr  17215  exmidcon  17216  exmidpeirce  17217  wexmiddc  17221  wexmiddiffi  17223  wexmiddifxylem  17224  wexmiddifxy  17225  nnsf  17227  nninfsellemdc  17232  nninffeq  17242  nnnninfen  17243  exmidsbthrlem  17246  sbthom  17250  triap  17257  trilpo  17272  apdifflemr  17276  redcwlpo  17285  tridceq  17286  nconstwlpolem0  17293  nconstwlpolem  17295  nconstwlpo  17296  neapmkv  17298  ltlenmkv  17300