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  mpnanrd  700  oibabs  722  dcim  849  dcstab  852  stdcndc  853  stdcndcOLD  854  dcand  941  dcor  944  dfifp2dc  990  3mix1  1193  3mix2  1194  3jca  1204  syl3anbrc  1208  syl21anbrc  1209  inegd  1417  pclem6  1419  xoranor  1422  dcfrompeirce  1495  nfxfrd  1524  nfd  1572  hban  1596  nfan1  1613  nford  1616  nfand  1617  hbim1  1619  nfal  1625  alexim  1694  nnal  1698  hbn  1699  nf4r  1719  19.34  1732  nfexd  1810  sbcof2  1859  nfsb2or  1886  sbidm  1900  nfdv  1926  nfd2  2076  nfeudv  2095  mon  2109  eumo  2112  mo23  2122  eu2  2125  eu3h  2126  exmodc  2131  exmonim  2132  mo2r  2133  mo3h  2134  bm1.1  2217  eqrdv  2230  3eltr4g  2318  abbi2dv  2353  abbi1dv  2354  nfcd  2379  nfcxfrd  2382  dcned  2418  neqned  2419  3netr4g  2447  necon3bi  2462  necon2ai  2466  nnral  2532  alral  2587  rspe  2591  rsp2e  2593  rgen2a  2596  ralrimi  2613  r19.27v  2670  r19.28v  2671  r19.27av  2678  r19.32r  2689  nfreudxy  2717  mormo  2760  nrexrmo  2765  cgsex2g  2849  cgsex4g  2850  spc2egv  2906  spc2gv  2907  spc3egv  2908  spc3gv  2909  rspce  2915  ceqex  2943  elrab3t  2971  elrabd  2974  mosubt  2993  mo2icl  2995  reu3  3006  reu6i  3007  2rmorex  3022  sbc5  3065  rspesbca  3127  rmo2ilem  3132  sbnfc2  3198  ssrd  3242  ssrdv  3243  3sstr4g  3280  eqsstrid  3283  ss2abdv  3310  abssdv  3311  rabssdv  3317  ss2rabdv  3318  ssun1  3381  unssad  3395  unssbd  3396  ssddif  3454  uneqin  3471  indifdir  3476  undif3ss  3481  reuss2  3500  n0rf  3520  reximdva0m  3523  rabxmdc  3539  ssindif0im  3567  minel  3569  ralidm  3609  ralm  3612  dcun  3618  ifmdc  3664  disjsn2  3751  rabsnif  3757  absneu  3762  rabsneu  3763  opprc  3903  elunii  3918  dfnfc2  3931  uniss2  3944  unidif  3945  ssunieq  3946  intab  3977  iunss2  4035  iunssd  4036  iunxdif2  4039  invdisj  4101  disjiun  4103  3brtr4g  4142  trin  4217  triun  4220  truni  4221  trint  4222  iinexgm  4265  class2seteq  4275  pwuni  4304  exmid1dc  4312  exmidn0m  4313  exmidsssn  4314  exmid0el  4316  exmidel  4317  exmidundif  4318  exmidundifim  4319  exmid1stab  4320  mss  4341  copsex2t  4360  euotd  4370  pwunim  4406  ispod  4424  sotricim  4443  exse  4456  frind  4472  trssord  4500  suctr  4541  pwnex  4569  eusvnf  4573  eusvnfb  4574  eusv2nf  4576  rexxfrd  4583  ralxfr2d  4584  rexxfr2d  4585  rabxfrd  4589  reuhypd  4591  eldifpw  4597  iunpw  4600  ssorduni  4608  onsucb  4624  onsucelsucr  4629  sucunielr  4631  ontriexmidim  4643  ordtri2or2exmidlem  4647  onsucelsucexmid  4651  reg2exmidlema  4655  setindel  4659  elirr  4662  orddisj  4667  en2lp  4675  suc11g  4678  ordsuc  4684  nlimsucg  4687  ordtri2or2exmid  4692  ontri2orexmidim  4693  zfregfr  4695  wessep  4699  tfi  4703  peano5  4719  limom  4735  peano2b  4736  nndceq0  4739  nnpredcl  4744  0nelrel  4795  eqrelrdv  4845  xpsspw  4861  relint  4875  relop  4904  eqbrrdva  4924  ssrelrn  4946  opeldm  4958  reldmm  4974  elres  5073  relssres  5075  elrelimasn  5127  exse2  5135  issref  5144  trin2  5153  dminss  5176  imainss  5177  rnxpid  5196  dmsn0el  5231  dmmptg  5259  relrelss  5288  cnviinm  5303  iotanul  5327  sniota  5342  dffun5r  5363  funmo  5366  funco  5391  funun  5396  fununmo  5397  fununfun  5398  funprg  5405  funtpg  5406  funtp  5408  fntpg  5411  fununi  5423  funcnvuni  5424  imadiflem  5434  imainlem  5436  funimaexglem  5438  isarep2  5442  fnunsn  5464  2elresin  5468  fnimadisj  5478  dmmptd  5488  fco  5526  funssxp  5531  fssres  5539  feu  5548  fimacnvdisj  5550  fabexg  5553  f00  5558  f0rn0  5561  f1co  5584  fores  5599  foco  5600  f1ores  5628  foimacnv  5631  f1oun  5633  fun11iun  5634  f1oco  5636  fo00  5651  brprcneu  5662  fv3  5692  relelfvdm  5701  nfvres  5705  nfunsn  5706  funfvbrb  5790  respreima  5804  dff2  5820  dff3im  5821  dffo4  5824  fvmptelcdm  5829  ffvresb  5839  f1oresrab  5841  fmptco  5842  fsn  5848  fcof  5862  fpr  5865  ftpg  5867  fsnunf  5883  fsnunfv  5884  elabrex  5929  dff1o6  5948  foeqcnvco  5962  fliftel1  5966  isores1  5986  isoini2  5991  riotasbc  6019  acexmidlemph  6042  acexmidlemcase  6044  oprabidlem  6080  brabvv  6098  eloprabga  6139  fnoprabg  6153  caovimo  6247  oprabexd  6319  uchoice  6330  fo1stresm  6354  fo2ndresm  6355  unielxp  6367  1st2ndbr  6377  opabn1stprc  6388  fmpoco  6411  1stconst  6416  2ndconst  6417  poxp  6427  spc2ed  6428  disjxp1  6431  elmpom  6433  suppsnopdc  6449  reldmtpos  6483  tposfun  6490  dftpos4  6493  smores  6522  smores2  6524  tfrlem1  6538  tfr0dm  6552  tfrlemibxssdm  6557  tfrlemibex  6559  tfrlemiubacc  6560  tfrlemi14d  6563  tfrexlem  6564  tfri1d  6565  tfr1onlembxssdm  6573  tfr1onlembex  6575  tfr1onlemubacc  6576  tfr1onlemres  6579  tfrcllemsucfn  6583  tfrcllembxssdm  6586  tfrcllembex  6588  tfrcllemubacc  6589  tfrcllemres  6592  tfri3  6597  rdgon  6616  frecabcl  6629  frecfcllem  6634  frecrdg  6638  2oconcl  6671  nnsucelsuc  6723  nntri3or  6725  nndceq  6731  nndcel  6732  dcdifsnid  6736  ecexr  6771  brdifun  6793  ecelqsdm  6838  iinerm  6840  eroveu  6859  erovlem  6860  ecopovtrn  6865  ecopovtrng  6868  th3qlem1  6870  pmsspw  6916  map0b  6920  mapsnd  6922  mapsn  6924  mapsncnv  6929  ixpf  6954  uniixp  6955  ixpexgg  6956  resixp  6967  f1oen3g  6992  ssdomg  7017  domtr  7024  snfig  7055  modom  7060  enpr2d  7063  dom1o  7068  xpf1o  7096  xpmapenlem  7101  php5dom  7116  fidceq  7123  nnfi  7126  fiunsnnn  7137  findcard  7144  findcard2  7145  findcard2s  7146  ac6sfi  7154  fidcen  7155  tridc  7156  fimax2gtri  7158  finexdc  7159  elssdc  7161  eqsndc  7162  exmidpw  7167  exmidpweq  7168  exmidpw2en  7171  nnwetri  7175  unsnfi  7178  unsnfidcex  7179  unsnfidcel  7180  undifdcss  7182  tpfidisj  7188  tpfidceq  7189  exmidssfi  7198  iunfidisj  7212  mapfi  7213  fissfi  7215  snexxph  7219  fidcenumlemrks  7222  sbthlem2  7227  sbthlemi3  7228  sbthlem7  7232  sbthlemi8  7233  fival  7256  dcfi  7267  supmoti  7283  djuss  7360  updjudhf  7369  updjud  7372  casefun  7375  caseinj  7379  omp1eomlem  7384  djufun  7394  djuinj  7396  ctssdccl  7401  ctfoex  7408  nnnninf  7416  nnnninfeq2  7419  nninfisollem0  7420  nninfisollemne  7421  nninfisollemeq  7422  nninfisol  7423  finomni  7430  exmidomniim  7431  exmidomni  7432  fodjuomnilemdc  7434  omniwomnimkv  7457  nninfdcinf  7461  nninfwlporlem  7463  nninfwlpoimlemg  7465  nninfwlpoim  7469  nninfinfwlpo  7470  exmidonfinlem  7495  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  finacn  7510  exmidaclem  7514  dju1en  7519  exmidontriimlem1  7527  exmidontriimlem3  7529  iftrueb01  7532  pw1on  7535  3nsssucpw1  7545  2omotaplemap  7570  2omotap  7572  exmidmotap  7574  cc4f  7582  cc4n  7584  acnccim  7585  dmaddpqlem  7691  nqpi  7692  dmaddpq  7693  dmmulpq  7694  ltdcnq  7711  subhalfnqq  7728  enq0sym  7746  enq0ref  7747  enq0tr  7748  nqnq0pi  7752  nq0nn  7756  addnq0mo  7761  mulnq0mo  7762  nqpnq0nq  7767  nqnq0a  7768  nqnq0m  7769  npsspw  7785  elnp1st2nd  7790  prnmaxl  7802  prnminu  7803  prarloc  7817  genprndl  7835  genprndu  7836  nqprm  7856  nqprl  7865  nqpru  7866  addnqprlemrl  7871  addnqprlemru  7872  prmuloc  7880  mulnqprlemrl  7887  mulnqprlemru  7888  ltsopr  7910  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemopu  7917  lteupri  7931  recexprlemopl  7939  recexprlemopu  7941  recexprlemdisj  7944  archpr  7957  cauappcvgprlemdisj  7965  cauappcvgprlemladdrl  7971  cauappcvgprlem2  7974  caucvgprlemnbj  7981  caucvgprlemdisj  7988  caucvgprlemladdfu  7991  caucvgprlem2  7994  caucvgprprlemnbj  8007  caucvgprprlemdisj  8016  suplocexprlemml  8030  suplocexprlemrl  8031  suplocexprlemmu  8032  suplocexprlemloc  8035  addsrmo  8057  mulsrmo  8058  recexgt0sr  8087  prsrpos  8099  caucvgsrlemasr  8104  suplocsrlemb  8120  suplocsrlempr  8121  suplocsr  8123  elrealeu  8143  pitonn  8162  pitoregt0  8163  pitore  8164  recnnre  8165  axaddcl  8178  axaddrcl  8179  axmulcl  8180  axmulrcl  8181  axrnegex  8193  axcnre  8195  axpre-lttrn  8198  rereceu  8203  axarch  8205  axpre-suploclemres  8215  axpre-suploc  8216  ltxrlt  8338  apirr  8878  divmulasscomap  8969  rerecclap  9003  lbreu  9218  arch  9492  0mnnnnn0  9527  nnm1nn0  9536  elnnnn0c  9540  elnnz1  9599  ztri3or0  9618  nzadd  9629  nn0n0n1ge2  9647  zdceq  9652  zdcle  9653  zdclt  9654  uzind  9688  eluzge3nn  9903  supinfneg  9926  infsupneg  9927  eluz2b2  9934  elnn1uz2  9938  elnn0dc  9942  elnndc  9943  nn01to3  9948  znq  9955  qaddcl  9966  qmulcl  9968  qreccl  9973  irradd  9977  irrmul  9978  elpq  9980  cnref1o  9982  xnn0dcle  10134  xrpnfdc  10174  xrmnfdc  10175  xaddcom  10193  xnegdi  10200  xpncan  10203  xleadd1a  10205  iooidg  10241  elioo4g  10266  elfzd  10349  fzdcel  10373  fznlem  10374  fzpreddisj  10404  fz0to4untppr  10457  elfz0ubfz0  10458  elfz0fzfz0  10459  fz0fzelfz0  10460  fz0fzdiffz0  10463  elfzmlbp  10465  difelfzle  10467  4fvwrd4  10473  fzosplit  10512  elfzo0  10519  nn0p1elfzo  10520  fzo1fzo0n0  10521  elfzonn0  10524  fzofzim  10526  elfzo1  10529  elfzom1elp1fzo  10546  fzossfzop1  10556  ssfzo12bi  10569  exfzdc  10585  zsupcllemstep  10588  infssuzex  10592  qdceq  10603  qdclt  10604  exbtwnzlemstep  10606  exbtwnzlemex  10608  exbtwnz  10609  rebtwn2zlemstep  10611  rebtwn2z  10613  qbtwnxr  10616  modfzo0difsn  10756  frec2uzrand  10766  frec2uzf1od  10767  frecuzrdgrcl  10771  frecuzrdgtcl  10773  frecuzrdgrclt  10776  frecuzrdgfunlem  10780  frecfzennn  10787  nninfinf  10804  seq3f1olemp  10876  seq3f1oleml  10877  seqf1oglem1  10880  ser0f  10895  expcl2lemap  10912  hashunsng  11170  sshashneg  11201  hashfibclem  11202  hashfibc  11203  iswrdinn0  11225  snopiswrd  11230  wrdlndm  11237  iswrdsymb  11238  wrdsymb1  11257  ccatfv0  11287  ccatval21sw  11289  lswccatn0lsw  11295  eqs1  11312  ccat1st1st  11325  lswccats1fst  11328  fzowrddc  11335  swrdfv0  11342  swrdlen2  11350  swrdfv2  11351  swrdsbslen  11354  swrdspsleq  11355  pfxfv0  11380  pfxtrcfv0  11382  pfxeq  11384  pfx1  11391  swrdswrdlem  11392  cats1un  11409  pfxccatin12lem2a  11415  pfxccatin12lem2  11419  pfxccatin12lem3  11420  swrdccat  11423  cats1fvn  11452  cats1fvnd  11453  shftfvalg  11499  shftfval  11502  caucvgre  11662  rexanuz  11669  recvguniq  11676  rennim  11683  resqrexlemf  11688  rsqrmo  11708  fimaxre2  11908  climeu  11977  sumdc  12039  summodc  12065  zsumdc  12066  isum  12067  fisumss  12074  isumss2  12075  fsumsplit  12089  sumsnf  12091  fsumsplitsn  12092  sumtp  12096  sumsplitdc  12114  fsum2dlemstep  12116  fisum0diag2  12129  fsumconst  12136  modfsummodlemstep  12139  fsum00  12144  fsumabs  12147  fsumiun  12159  isumlessdc  12178  expcnv  12186  prodmodc  12260  zproddc  12261  iprodap  12262  iprodap0  12264  fprodssdc  12272  prodsnf  12274  fprodsplitdc  12278  fprodsplit  12279  fprodm1  12280  fprod1p  12281  fprodunsn  12286  fprod2dlemstep  12304  fprodsplitsn  12315  ef0lem  12342  modmulconst  12505  dvdsdivcl  12532  dvdsssfz1  12534  dvdsfac  12542  zeoxor  12551  nn0ehalf  12585  nn0oddm1d2  12591  nnoddm1d2  12592  divalglemeunn  12603  divalglemeuneg  12605  bitsfzolem  12636  bitsinv1  12644  gcdsupex  12649  gcdsupcl  12650  bezoutlemnewy  12688  bezoutlemmain  12690  bezoutlemeu  12699  dfgcd2  12706  nnwosdc  12731  nninfct  12733  algrf  12738  algcvgblem  12742  lcmgcdlem  12770  lcmdvds  12772  coprmgcdb  12781  mulgcddvds  12787  qredeu  12790  cncongr1  12796  cncongr2  12797  isprm2lem  12809  dvdsnprmd  12818  prmdc  12823  oddprmge3  12828  pw2dvdseu  12861  phibndlem  12909  dfphi2  12913  hashdvds  12914  phiprmpw  12915  eulerthlemh  12924  hashgcdeq  12933  phisum  12934  odzdvds  12939  reumodprminv  12947  nnnn0modprm0  12949  prm23ge5  12958  pclemdc  12982  pcdvdsb  13014  difsqpwdvds  13032  oddprmdvds  13048  1arith  13061  4sqlem3  13084  4sqlemafi  13089  4sqlemffi  13090  4sqleminfi  13091  4sqexercise1  13092  4sqlem11  13095  4sqlem19  13103  ennnfonelemdc  13142  ennnfonelemh  13147  ennnfonelemhf1o  13156  ennnfonelemf1  13161  ennnfonelemrn  13162  ennnfonelemdm  13163  exmidunben  13169  ctinfomlemom  13170  ctinfom  13171  ctiunctlemudc  13180  ctiunctlemf  13181  ctiunctal  13184  nninfdclemcl  13191  nninfdclemf  13192  nninfdclemp1  13193  isstructim  13218  setsresg  13242  strleund  13308  1strbas  13322  2strbasg  13325  2stropg  13326  restsspw  13454  tgval  13467  ptex  13469  imasaddfnlemg  13519  fnpr2o  13544  fnpr2ob  13545  mgmidsssn0  13589  fngsum  13593  igsumvalx  13594  isnsgrp  13611  sgrpidmndm  13625  mndinvmod  13650  mnd1  13660  mhmeql  13697  grpinveu  13743  prdsinvlem  13813  mulgval  13831  subgintm  13907  trivsubgsnd  13910  eqgfval  13931  ecqusaddd  13947  ecqusaddcl  13948  ghmeql  13976  iscmnd  14007  imasabl  14045  gsumfzmhm2  14053  rnglz  14081  srgfcl  14109  rhmopp  14313  subrgdvds  14372  lssuni  14503  lssintclm  14524  lspf  14529  qusmulrng  14672  mulgrhm2  14750  znf1o  14791  psrbagfi  14815  psrbagconcl  14819  psr1clfi  14835  mplsubgfilemcl  14846  istopon  14870  toponcom  14884  topgele  14886  topontopn  14894  tsettps  14895  eltg2b  14911  unitg  14919  tgss2  14936  bastop2  14941  distop  14942  epttop  14947  cldss2  14963  neisspw  15005  neipsm  15011  neiuni  15018  tgcn  15065  tgcnp  15066  cnntr  15082  lmff  15106  txuni2  15113  txbasex  15114  txbas  15115  txcnp  15128  txcnmpt  15130  txcn  15132  txdis  15134  txdis1cn  15135  cnmpt11  15140  cnmpt12  15144  cnmpt21  15148  cnmpt2t  15150  cnmpt22  15151  blsscls2  15350  xmetxpbl  15365  xmettxlem  15366  tgqioo  15412  fsumcncntop  15424  cncfmpt1f  15455  mulcncflem  15464  mulcncf  15465  dedekindeu  15480  dedekindicclemicc  15489  dedekindicc  15490  ivthinclemdisj  15497  hovercncf  15503  limcimo  15522  cnmptlimc  15531  reldvg  15536  dvfvalap  15538  dvfgg  15545  dvmptfsum  15582  dveflem  15583  dvef  15584  elply2  15592  sincn  15626  coscn  15627  reeff1o  15630  pilem3  15640  ioocosf1o  15711  mpodvdsmulf1o  15850  fsumdvdsmul  15851  perfectlem2  15860  lgsne0  15903  gausslemma2dlem1a  15923  gausslemma2dlem4  15929  lgseisenlem2  15936  lgseisenlem3  15937  lgsquadlem2  15943  2lgslem3  15966  2sqlem2  15980  mul2sq  15981  2sqlem3  15982  2sqlem7  15986  edgstruct  16051  pw0ss  16070  incistruhgr  16077  upgrex  16090  umgrnloop0  16104  upgr1een  16111  lfgrnloopen  16120  umgredg  16132  umgrnloop2  16138  uspgredgiedg  16165  uspgriedgedg  16166  usgrislfuspgrdom  16177  usgredg3  16201  uspgredg2vlem  16207  uspgredg2v  16208  ushgredgedg  16213  ushgredgedgloop  16215  uhgr0vsize0en  16222  usgr1e  16228  subusgr  16262  vtxedgfi  16276  vtxlpfi  16277  vtxdumgrfival  16285  1loopgrvd2fi  16292  p1evtxdeqfilem  16298  vdegp1aid  16301  wlkcprim  16337  wlk1walkdom  16346  uspgr2wlkeq  16352  upgr2wlkdc  16364  wlkres  16366  clwwlkccatlem  16387  clwwlknp  16404  umgr2cwwk2dif  16411  trlsegvdegfi  16454  eupth2lem3lem3fi  16457  eupth2lem3lem6fi  16458  eupth2lem3lem4fi  16460  eupth2lembfi  16464  depindlem1  16493  bj-trst  16503  bj-fast  16505  bj-stand  16512  bj-trdc  16516  bj-fadc  16518  decidr  16560  djulclALT  16565  djurclALT  16566  bj-charfunr  16572  bj-indind  16694  bj-2inf  16700  bj-nntrans2  16714  bj-peano4  16717  bj-nnord  16720  bj-inf2vn  16736  bj-inf2vn2  16737  bj-findis  16741  pwf1oexmid  16765  subctctexmid  16766  pw1dceq  16770  exmidnotnotr  16771  exmidcon  16772  exmidpeirce  16773  nnsf  16775  nninfsellemdc  16780  nninffeq  16790  nnnninfen  16791  exmidsbthrlem  16794  sbthom  16798  triap  16805  trilpo  16819  apdifflemr  16823  redcwlpo  16832  tridceq  16833  nconstwlpolem0  16840  nconstwlpolem  16842  nconstwlpo  16843  neapmkv  16845  ltlenmkv  16847  gfsump1  16859