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  sn0disj  4127  3brtr4g  4165  trin  4241  triun  4244  truni  4245  trint  4246  iinexgm  4292  class2seteq  4302  pwuni  4331  exmid1dc  4339  exmidn0m  4340  exmidsssn  4341  exmid0el  4343  exmidel  4344  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  mss  4368  copsex2t  4387  euotd  4397  pwunim  4433  ispod  4451  sotricim  4470  exse  4483  frind  4499  trssord  4527  suctr  4568  pwnex  4597  eusvnf  4601  eusvnfb  4602  eusv2nf  4604  rexxfrd  4611  ralxfr2d  4612  rexxfr2d  4613  rabxfrd  4617  reuhypd  4619  eldifpw  4625  iunpw  4628  ssorduni  4636  onsucb  4652  onsucelsucr  4657  sucunielr  4659  ontriexmidim  4671  ordtri2or2exmidlem  4675  onsucelsucexmid  4679  reg2exmidlema  4683  setindel  4687  elirr  4690  orddisj  4695  en2lp  4703  suc11g  4706  ordsuc  4712  nlimsucg  4715  ordtri2or2exmid  4720  ontri2orexmidim  4721  zfregfr  4723  wessep  4727  tfi  4731  peano5  4747  limom  4763  peano2b  4764  nndceq0  4767  nnpredcl  4772  0nelrel  4823  eqrelrdv  4873  xpsspw  4889  relint  4903  relop  4932  eqbrrdva  4952  ssrelrn  4974  opeldm  4986  reldmm  5002  elres  5101  relssres  5103  elrelimasn  5156  exse2  5164  issref  5173  trin2  5182  dminss  5205  imainss  5206  rnxpid  5225  dmsn0el  5260  dmmptg  5288  relrelss  5317  cnviinm  5332  iotanul  5356  sniota  5371  dffun5r  5392  funmo  5395  funco  5420  funun  5425  fununmo  5426  fununfun  5427  funprg  5434  funtpg  5435  funtp  5437  fntpg  5440  fununi  5452  funcnvuni  5453  imadiflem  5463  imainlem  5465  funimaexglem  5467  isarep2  5471  fnunsn  5493  2elresin  5497  fnimadisj  5507  dmmptd  5517  fco  5555  funssxp  5560  fssres  5568  feu  5577  fimacnvdisj  5579  fabexg  5582  f00  5587  f0rn0  5590  f1co  5613  fores  5628  foco  5629  f1ores  5657  foimacnv  5660  f1oun  5662  fun11iun  5663  f1oco  5665  fo00  5680  brprcneu  5691  fv3  5721  relelfvdm  5730  nfvres  5735  nfunsn  5736  funfvbrb  5825  respreima  5839  dff2  5855  dff3im  5856  dffo4  5859  fvmptelcdm  5864  ffvresb  5874  f1oresrab  5876  fmptco  5877  fsn  5883  fcof  5897  fpr  5900  ftpg  5902  fsnunf  5918  fsnunfv  5919  elabrex  5966  dff1o6  5985  foeqcnvco  5999  fliftel1  6003  isores1  6023  isoini2  6028  riotasbc  6058  acexmidlemph  6081  acexmidlemcase  6083  oprabidlem  6119  brabvv  6137  eloprabga  6178  fnoprabg  6192  caovimo  6286  oprabexd  6364  uchoice  6375  fo1stresm  6399  fo2ndresm  6400  unielxp  6412  1st2ndbr  6422  opabn1stprc  6433  fmpoco  6456  1stconst  6461  2ndconst  6462  poxp  6472  spc2ed  6473  disjxp1  6476  elmpom  6478  suppsnopdc  6494  reldmtpos  6528  tposfun  6535  dftpos4  6538  smores  6567  smores2  6569  tfrlem1  6583  tfr0dm  6597  tfrlemibxssdm  6602  tfrlemibex  6604  tfrlemiubacc  6605  tfrlemi14d  6608  tfrexlem  6609  tfri1d  6610  tfr1onlembxssdm  6618  tfr1onlembex  6620  tfr1onlemubacc  6621  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllembxssdm  6631  tfrcllembex  6633  tfrcllemubacc  6634  tfrcllemres  6637  tfri3  6642  rdgon  6661  frecabcl  6674  frecfcllem  6679  frecrdg  6683  2oconcl  6716  nnsucelsuc  6768  nntri3or  6770  nndceq  6776  nndcel  6777  dcdifsnid  6781  ecexr  6816  brdifun  6838  ecelqsdm  6883  iinerm  6885  eroveu  6904  erovlem  6905  ecopovtrn  6910  ecopovtrng  6913  th3qlem1  6915  fsetdmprc0  6954  pmsspw  6968  map0b  6972  mapsnd  6974  mapsn  6976  mapsncnv  6981  ixpf  7006  uniixp  7007  ixpexgg  7008  resixp  7019  f1oen3g  7044  ssdomg  7069  domtr  7076  snfig  7107  modom  7112  enpr2d  7115  dom1o  7120  xpf1o  7148  xpmapenlem  7153  php5dom  7168  fidceq  7175  nnfi  7178  fiunsnnn  7189  findcard  7196  findcard2  7197  findcard2s  7198  ac6sfi  7206  fidcen  7207  tridc  7208  fimax2gtri  7210  finexdc  7211  elssdc  7213  eqsndc  7214  exmidpw  7219  exmidpweq  7220  exmidpw2en  7223  nnwetri  7227  unsnfi  7230  unsnfidcex  7231  unsnfidcel  7232  undifdcss  7234  tpfidisj  7240  tpfidceq  7241  exmidssfi  7250  iunfidisj  7264  mapfi  7265  fissfi  7267  snexxph  7272  fidcenumlemrks  7275  sbthlem2  7280  sbthlemi3  7281  sbthlem7  7285  sbthlemi8  7286  fival  7309  dcfi  7320  fdcf1  7321  f1setfi  7322  supmoti  7339  djuss  7416  updjudhf  7425  updjud  7428  casefun  7431  caseinj  7435  omp1eomlem  7440  djufun  7450  djuinj  7452  ctssdccl  7457  ctfoex  7464  nnnninf  7472  nnnninfeq2  7475  nninfisollem0  7476  nninfisollemne  7477  nninfisollemeq  7478  nninfisol  7479  finomni  7486  exmidomniim  7487  exmidomni  7488  fodjuomnilemdc  7490  omniwomnimkv  7513  nninfdcinf  7517  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoim  7525  nninfinfwlpo  7526  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  finacn  7566  exmidaclem  7570  dju1en  7575  exmidontriimlem1  7583  exmidontriimlem3  7585  iftrueb01  7588  pw1on  7591  3nsssucpw1  7601  2omotaplemap  7629  2omotap  7631  exmidmotap  7633  cc4f  7641  cc4n  7643  acnccim  7644  dmaddpqlem  7750  nqpi  7751  dmaddpq  7752  dmmulpq  7753  ltdcnq  7770  subhalfnqq  7787  enq0sym  7805  enq0ref  7806  enq0tr  7807  nqnq0pi  7811  nq0nn  7815  addnq0mo  7820  mulnq0mo  7821  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  npsspw  7844  elnp1st2nd  7849  prnmaxl  7861  prnminu  7862  prarloc  7876  genprndl  7894  genprndu  7895  nqprm  7915  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  prmuloc  7939  mulnqprlemrl  7946  mulnqprlemru  7947  ltsopr  7969  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  lteupri  7990  recexprlemopl  7998  recexprlemopu  8000  recexprlemdisj  8003  archpr  8016  cauappcvgprlemdisj  8024  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemnbj  8040  caucvgprlemdisj  8047  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemnbj  8066  caucvgprprlemdisj  8075  suplocexprlemml  8089  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemloc  8094  addsrmo  8116  mulsrmo  8117  recexgt0sr  8146  prsrpos  8158  caucvgsrlemasr  8163  suplocsrlemb  8179  suplocsrlempr  8180  suplocsr  8182  elrealeu  8202  pitonn  8221  pitoregt0  8222  pitore  8223  recnnre  8224  axaddcl  8237  axaddrcl  8238  axmulcl  8239  axmulrcl  8240  axrnegex  8252  axcnre  8254  axpre-lttrn  8257  rereceu  8262  axarch  8264  axpre-suploclemres  8274  axpre-suploc  8275  ltxrlt  8397  apirr  8941  divmulasscomap  9034  rerecclap  9068  lbreu  9283  indconst1  9312  arch  9571  0mnnnnn0  9606  nnm1nn0  9615  elnnnn0c  9619  elnnz1  9678  ztri3or0  9697  nzadd  9708  nn0n0n1ge2  9726  zdceq  9731  zdcle  9732  zdclt  9733  uzind  9768  eluzge3nn  9988  supinfneg  10011  infsupneg  10012  eluz2b2  10019  elnn1uz2  10023  elnn0dc  10027  elnndc  10028  nn01to3  10033  znq  10040  qaddcl  10051  qmulcl  10053  qreccl  10058  irradd  10062  irrmul  10064  elpq  10066  cnref1o  10068  xnn0dcle  10221  xrpnfdc  10261  xrmnfdc  10262  xaddcom  10280  xnegdi  10287  xpncan  10290  xleadd1a  10292  iooidg  10328  elioo4g  10353  elfzd  10436  fzdcel  10461  fznlem  10462  fzpreddisj  10495  fz0to4untppr  10548  elfz0ubfz0  10549  elfz0fzfz0  10550  fz0fzelfz0  10551  fz0fzdiffz0  10554  elfzmlbp  10556  difelfzle  10558  4fvwrd4  10564  fzosplit  10603  elfzo0  10610  nn0p1elfzo  10611  fzo1fzo0n0  10612  elfzonn0  10615  fzofzim  10617  elfzo1  10620  elfzom1elp1fzo  10637  fzossfzop1  10647  ssfzo12bi  10660  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  qdceq  10696  qdclt  10697  exbtwnzlemstep  10699  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnxr  10709  modfzo0difsn  10853  frec2uzrand  10863  frec2uzf1od  10864  frecuzrdgrcl  10868  frecuzrdgtcl  10870  frecuzrdgrclt  10873  frecuzrdgfunlem  10877  frecfzennn  10884  nninfinf  10901  seq3f1olemp  10973  seq3f1oleml  10974  seqf1oglem1  10977  ser0f  10992  expcl2lemap  11009  hashunsng  11270  hashmap  11290  sshashneg  11303  hashfibclem  11304  hashfibc  11305  hashf1lem1  11307  hashf1lem2  11308  iswrdinn0  11331  snopiswrd  11336  wrdlndm  11343  iswrdsymb  11344  wrdsymb1  11363  ccatfv0  11393  ccatval21sw  11395  lswccatn0lsw  11401  eqs1  11418  ccat1st1st  11431  lswccats1fst  11434  fzowrddc  11441  swrdfv0  11448  swrdlen2  11456  swrdfv2  11457  swrdsbslen  11460  swrdspsleq  11461  pfxfv0  11486  pfxtrcfv0  11488  pfxeq  11490  pfx1  11497  swrdswrdlem  11498  cats1un  11515  pfxccatin12lem2a  11521  pfxccatin12lem2  11525  pfxccatin12lem3  11526  swrdccat  11529  cats1fvn  11558  cats1fvnd  11559  shftfvalg  11605  shftfval  11608  caucvgre  11769  rexanuz  11776  recvguniq  11783  rennim  11790  resqrexlemf  11795  rsqrmo  11815  fimaxre2  12016  climeu  12087  sumdc  12149  summodc  12175  zsumdc  12176  isum  12177  fisumss  12184  isumss2  12185  fsumsplit  12199  sumsnf  12201  fsumsplitsn  12202  sumtp  12206  sumsplitdc  12224  fsum2dlemstep  12226  fisum0diag2  12239  fsumconst  12246  modfsummodlemstep  12249  fsum00  12254  fsumabs  12257  fsumiun  12269  isumlessdc  12288  expcnv  12296  prodmodc  12370  zproddc  12371  iprodap  12372  iprodap0  12374  fprodssdc  12382  prodsnf  12384  fprodsplitdc  12388  fprodsplit  12389  fprodm1  12390  fprod1p  12391  fprodunsn  12396  fprod2dlemstep  12414  fprodsplitsn  12425  ef0lem  12452  modmulconst  12615  dvdsdivcl  12642  dvdsssfz1  12644  dvdsfac  12652  zeoxor  12661  nn0ehalf  12695  nn0oddm1d2  12701  nnoddm1d2  12702  divalglemeunn  12713  divalglemeuneg  12715  bitsfzolem  12746  bitsinv1  12754  gcdsupex  12759  gcdsupcl  12760  bezoutlemnewy  12798  bezoutlemmain  12800  bezoutlemeu  12809  dfgcd2  12816  nnwosdc  12841  nninfct  12843  algrf  12848  algcvgblem  12852  lcmgcdlem  12880  lcmdvds  12882  coprmgcdb  12891  mulgcddvds  12897  qredeu  12900  cncongr1  12906  cncongr2  12907  isprm2lem  12919  dvdsnprmd  12928  prmdc  12933  prmdcz  12934  oddprmge3  12939  pwbdvdseu  12972  nn0sqdcq  13013  phibndlem  13023  dfphi2  13027  hashdvds  13028  phiprmpw  13029  eulerthlemh  13038  hashgcdeq  13047  phisum  13048  odzdvds  13053  reumodprminv  13061  nnnn0modprm0  13063  prm23ge5  13072  pclemdc  13096  pcdvdsb  13128  difsqpwdvds  13146  oddprmdvds  13162  1arith  13175  4sqlem3  13198  4sqlemafi  13203  4sqlemffi  13204  4sqleminfi  13205  4sqexercise1  13206  4sqlem11  13209  4sqlem19  13217  ballotfilemcdc  13281  ballotfilemdifcfi  13283  ballotfilemdifcfz  13285  ballotfilem2  13286  ballotfilemiex  13302  ballotfilemscl  13305  ballotfilemth  13339  ennnfonelemdc  13348  ennnfonelemh  13353  ennnfonelemhf1o  13362  ennnfonelemf1  13367  ennnfonelemrn  13368  ennnfonelemdm  13369  exmidunben  13375  ctinfomlemom  13376  ctinfom  13377  ctiunctlemudc  13386  ctiunctlemf  13387  ctiunctal  13390  nninfdclemcl  13397  nninfdclemf  13398  nninfdclemp1  13399  isstructim  13424  setsresg  13448  strleund  13516  1strbas  13530  2strbasg  13533  2stropg  13534  restsspw  13662  tgval  13675  ptex  13677  imasaddfnlemg  13694  fnpr2o  13719  fnpr2ob  13720  mgmidsssn0  13763  fngzsum  13767  gzsumvalx  13768  isnsgrp  13780  sgrpidmndm  13792  mndinvmod  13817  mnd1  13821  mhmeql  13858  grpinveu  13902  mulgval  13984  subgintm  14060  trivsubgsnd  14063  eqgfval  14084  ecqusaddd  14100  ecqusaddcl  14101  ghmeql  14129  iscmnd  14191  imasabl  14230  gzsummhm2  14236  gsump1  14247  gsummptfidmsplit  14254  gsumsnfdcmn  14257  gsumunsnfd  14259  gsummhm2fi  14265  gsum2dfilem2  14272  gsumcom2fi  14275  prdsinvlem  14303  rnglz  14351  srgfcl  14384  rhmopp  14592  opprlring  14613  subrgdvds  14652  lssuni  14809  lssintclm  14830  lspf  14835  qusmulrng  14978  mulgrhm2  15054  znf1o  15095  aspid  15126  psrbagfi  15168  psrbagconcl  15173  psr1clfi  15198  mplsubgfilemcl  15215  istopon  15239  toponcom  15253  topgele  15255  topontopn  15263  tsettps  15264  eltg2b  15280  unitg  15288  tgss2  15305  bastop2  15310  distop  15311  epttop  15316  cldss2  15332  neisspw  15374  neipsm  15380  neiuni  15387  tgcn  15434  tgcnp  15435  cnntr  15451  lmff  15475  txuni2  15482  txbasex  15483  txbas  15484  txcnp  15497  txcnmpt  15499  txcn  15501  txdis  15503  txdis1cn  15504  cnmpt11  15509  cnmpt12  15513  cnmpt21  15517  cnmpt2t  15519  cnmpt22  15520  blsscls2  15719  xmetxpbl  15734  xmettxlem  15735  tgqioo  15781  fsumcncntop  15793  cncfmpt1f  15824  mulcncflem  15833  mulcncf  15834  dedekindeu  15849  dedekindicclemicc  15858  dedekindicc  15859  ivthinclemdisj  15866  hovercncf  15872  limcimo  15891  cnmptlimc  15900  reldvg  15905  dvfvalap  15907  dvfgg  15914  dvmptfsum  15951  dveflem  15952  dvef  15953  elply2  15961  sincn  15995  coscn  15996  reeff1o  15999  pilem3  16010  ioocosf1o  16082  ppiqfi  16242  prmdvdsfi  16243  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  chtdif  16264  efchtqdvds  16265  ppidif  16269  prmorcht  16282  mpodvdsmulf1o  16284  fsumdvdsmul  16285  ppiqub  16293  perfectlem2  16300  bcmono  16304  bpos  16320  lgsne0  16362  gausslemma2dlem1a  16382  gausslemma2dlem4  16388  lgseisenlem2  16395  lgseisenlem3  16396  lgsquadlem2  16402  2lgslem3  16425  2sqlem2  16439  mul2sq  16440  2sqlem3  16441  2sqlem7  16445  edgstruct  16510  pw0ss  16529  incistruhgr  16536  upgrex  16549  umgrnloop0  16563  upgr1een  16570  lfgrnloopen  16579  umgredg  16591  umgrnloop2  16597  uspgredgiedg  16624  uspgriedgedg  16625  usgrislfuspgrdom  16636  usgredg3  16660  uspgredg2vlem  16666  uspgredg2v  16667  ushgredgedg  16672  ushgredgedgloop  16674  uhgr0vsize0en  16681  usgr1e  16687  subusgr  16721  vtxedgfi  16735  vtxlpfi  16736  vtxdumgrfival  16744  1loopgrvd2fi  16751  p1evtxdeqfilem  16757  vdegp1aid  16760  wlkcprim  16796  wlk1walkdom  16805  uspgr2wlkeq  16811  upgr2wlkdc  16823  wlkres  16825  clwwlkccatlem  16846  clwwlknp  16863  umgr2cwwk2dif  16870  trlsegvdegfi  16913  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  eupth2lembfi  16923  depindlem1  16952  bj-trst  16972  bj-fast  16974  bj-stand  16981  bj-trdc  16985  bj-fadc  16987  decidr  17029  djulclALT  17034  djurclALT  17035  bj-charfunr  17041  bj-indind  17163  bj-2inf  17169  bj-nntrans2  17183  bj-peano4  17186  bj-nnord  17189  bj-inf2vn  17205  bj-inf2vn2  17206  bj-findis  17210  pwf1oexmid  17234  subctctexmid  17235  pw1dceq  17240  exmidnotnotr  17241  exmidcon  17242  exmidpeirce  17243  wexmiddc  17247  wexmiddiffi  17249  wexmiddifxylem  17250  wexmiddifxy  17251  nnsf  17254  nninfsellemdc  17259  nninffeq  17269  nnnninfen  17270  exmidsbthrlem  17273  sbthom  17277  triap  17284  trilpo  17299  apdifflemr  17303  redcwlpo  17312  tridceq  17313  nconstwlpolem0  17320  nconstwlpolem  17322  nconstwlpo  17323  neapmkv  17325  ltlenmkv  17327