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  714  dcim  841  dcstab  844  stdcndc  845  stdcndcOLD  846  dcor  935  3mix1  1166  3mix2  1167  3jca  1177  syl3anbrc  1181  syl21anbrc  1182  inegd  1372  pclem6  1374  xoranor  1377  nfxfrd  1475  nfd  1523  hban  1547  nfan1  1564  nford  1567  nfand  1568  hbim1  1570  nfal  1576  alexim  1645  nnal  1649  ax6blem  1650  nf4r  1671  19.34  1684  nfexd  1761  sbcof2  1810  nfsb2or  1837  sbidm  1851  nfdv  1877  nfd2  2022  nfeudv  2041  mon  2055  eumo  2058  mo23  2067  eu2  2070  eu3h  2071  exmodc  2076  exmonim  2077  mo2r  2078  mo3h  2079  bm1.1  2162  eqrdv  2175  3eltr4g  2263  abbi2dv  2296  abbi1dv  2297  nfcd  2314  nfcxfrd  2317  dcned  2353  neqned  2354  3netr4g  2382  necon3bi  2397  necon2ai  2401  nnral  2467  alral  2522  rspe  2526  rsp2e  2528  rgen2a  2531  ralrimi  2548  r19.27v  2604  r19.28v  2605  r19.27av  2612  r19.32r  2623  nfreudxy  2651  mormo  2689  nrexrmo  2694  cgsex2g  2775  cgsex4g  2776  spc2egv  2829  spc2gv  2830  spc3egv  2831  spc3gv  2832  rspce  2838  ceqex  2866  elrab3t  2894  elrabd  2897  mosubt  2916  mo2icl  2918  reu3  2929  reu6i  2930  2rmorex  2945  sbc5  2988  rspesbca  3049  rmo2ilem  3054  sbnfc2  3119  ssrd  3162  ssrdv  3163  3sstr4g  3200  eqsstrid  3203  ss2abdv  3230  abssdv  3231  rabssdv  3237  ss2rabdv  3238  ssun1  3300  unssad  3314  unssbd  3315  ssddif  3371  uneqin  3388  indifdir  3393  undif3ss  3398  reuss2  3417  n0rf  3437  reximdva0m  3440  rabxmdc  3456  ssindif0im  3484  minel  3486  ralidm  3525  ralm  3529  dcun  3535  ifmdc  3576  disjsn2  3657  absneu  3666  rabsneu  3667  opprc  3801  elunii  3816  dfnfc2  3829  uniss2  3842  unidif  3843  ssunieq  3844  intab  3875  iunss2  3933  iunssd  3934  iunxdif2  3937  invdisj  3999  disjiun  4000  3brtr4g  4039  trin  4113  triun  4116  truni  4117  trint  4118  iinexgm  4156  class2seteq  4165  pwuni  4194  exmid1dc  4202  exmidn0m  4203  exmidsssn  4204  exmid0el  4206  exmidel  4207  exmidundif  4208  exmidundifim  4209  exmid1stab  4210  mss  4228  copsex2t  4247  euotd  4256  pwunim  4288  ispod  4306  sotricim  4325  exse  4338  frind  4354  trssord  4382  suctr  4423  pwnex  4451  eusvnf  4455  eusvnfb  4456  eusv2nf  4458  rexxfrd  4465  ralxfr2d  4466  rexxfr2d  4467  rabxfrd  4471  reuhypd  4473  eldifpw  4479  iunpw  4482  ssorduni  4488  onsucb  4504  onsucelsucr  4509  sucunielr  4511  ontriexmidim  4523  ordtri2or2exmidlem  4527  onsucelsucexmid  4531  reg2exmidlema  4535  setindel  4539  elirr  4542  orddisj  4547  en2lp  4555  suc11g  4558  ordsuc  4564  nlimsucg  4567  ordtri2or2exmid  4572  ontri2orexmidim  4573  zfregfr  4575  wessep  4579  tfi  4583  peano5  4599  limom  4615  peano2b  4616  nndceq0  4619  nnpredcl  4624  0nelrel  4674  eqrelrdv  4724  xpsspw  4740  relint  4752  relop  4779  eqbrrdva  4799  opeldm  4832  elres  4945  relssres  4947  elrelimasn  4996  exse2  5004  issref  5013  trin2  5022  dminss  5045  imainss  5046  rnxpid  5065  dmsn0el  5100  dmmptg  5128  relrelss  5157  cnviinm  5172  iotanul  5195  sniota  5209  dffun5r  5230  funmo  5233  funco  5258  funun  5262  funprg  5268  funtpg  5269  funtp  5271  fntpg  5274  fununi  5286  funcnvuni  5287  imadiflem  5297  imainlem  5299  funimaexglem  5301  isarep2  5305  fnunsn  5325  2elresin  5329  fnimadisj  5338  dmmptd  5348  fco  5383  funssxp  5387  fssres  5393  feu  5400  fimacnvdisj  5402  fabexg  5405  f00  5409  f0rn0  5412  f1co  5435  fores  5449  foco  5450  f1ores  5478  foimacnv  5481  f1oun  5483  fun11iun  5484  f1oco  5486  fo00  5499  brprcneu  5510  fv3  5540  relelfvdm  5549  nfvres  5550  nfunsn  5551  funfvbrb  5631  respreima  5646  dff2  5662  dff3im  5663  dffo4  5666  fvmptelcdm  5671  ffvresb  5681  f1oresrab  5683  fmptco  5684  fsn  5690  fpr  5700  ftpg  5702  fsnunf  5718  fsnunfv  5719  elabrex  5760  dff1o6  5779  foeqcnvco  5793  fliftel1  5797  isores1  5817  isoini2  5822  riotasbc  5848  acexmidlemph  5870  acexmidlemcase  5872  oprabidlem  5908  brabvv  5923  eloprabga  5964  fnoprabg  5978  caovimo  6070  oprabexd  6130  fo1stresm  6164  fo2ndresm  6165  unielxp  6177  1st2ndbr  6187  fmpoco  6219  1stconst  6224  2ndconst  6225  poxp  6235  spc2ed  6236  disjxp1  6239  reldmtpos  6256  tposfun  6263  dftpos4  6266  smores  6295  smores2  6297  tfrlem1  6311  tfr0dm  6325  tfrlemibxssdm  6330  tfrlemibex  6332  tfrlemiubacc  6333  tfrlemi14d  6336  tfrexlem  6337  tfri1d  6338  tfr1onlembxssdm  6346  tfr1onlembex  6348  tfr1onlemubacc  6349  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllembxssdm  6359  tfrcllembex  6361  tfrcllemubacc  6362  tfrcllemres  6365  tfri3  6370  rdgon  6389  frecabcl  6402  frecfcllem  6407  frecrdg  6411  2oconcl  6442  nnsucelsuc  6494  nntri3or  6496  nndceq  6502  nndcel  6503  dcdifsnid  6507  ecexr  6542  brdifun  6564  ecelqsdm  6607  iinerm  6609  eroveu  6628  erovlem  6629  ecopovtrn  6634  ecopovtrng  6637  th3qlem1  6639  pmsspw  6685  map0b  6689  mapsn  6692  mapsncnv  6697  ixpf  6722  uniixp  6723  ixpexgg  6724  resixp  6735  f1oen3g  6756  ssdomg  6780  domtr  6787  snfig  6816  enpr2d  6819  xpf1o  6846  xpmapenlem  6851  php5dom  6865  fidceq  6871  nnfi  6874  fiunsnnn  6883  findcard  6890  findcard2  6891  findcard2s  6892  ac6sfi  6900  tridc  6901  fimax2gtri  6903  finexdc  6904  exmidpw  6910  exmidpweq  6911  nnwetri  6917  unsnfi  6920  unsnfidcex  6921  unsnfidcel  6922  undifdcss  6924  tpfidisj  6929  iunfidisj  6947  snexxph  6951  fidcenumlemrks  6954  sbthlem2  6959  sbthlemi3  6960  sbthlem7  6964  sbthlemi8  6965  fival  6971  dcfi  6982  supmoti  6994  djuss  7071  updjudhf  7080  updjud  7083  casefun  7086  caseinj  7090  omp1eomlem  7095  djufun  7105  djuinj  7107  ctssdccl  7112  ctfoex  7119  nnnninf  7126  nnnninfeq2  7129  nninfisollem0  7130  nninfisollemne  7131  nninfisollemeq  7132  nninfisol  7133  finomni  7140  exmidomniim  7141  exmidomni  7142  fodjuomnilemdc  7144  omniwomnimkv  7167  nninfdcinf  7171  nninfwlporlem  7173  nninfwlpoimlemg  7175  nninfwlpoim  7178  exmidonfinlem  7194  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  dju1en  7214  exmidontriimlem1  7222  exmidontriimlem3  7224  pw1on  7227  3nsssucpw1  7237  2omotaplemap  7258  2omotap  7260  exmidmotap  7262  cc4f  7270  cc4n  7272  dmaddpqlem  7378  nqpi  7379  dmaddpq  7380  dmmulpq  7381  ltdcnq  7398  subhalfnqq  7415  enq0sym  7433  enq0ref  7434  enq0tr  7435  nqnq0pi  7439  nq0nn  7443  addnq0mo  7448  mulnq0mo  7449  nqpnq0nq  7454  nqnq0a  7455  nqnq0m  7456  npsspw  7472  elnp1st2nd  7477  prnmaxl  7489  prnminu  7490  prarloc  7504  genprndl  7522  genprndu  7523  nqprm  7543  nqprl  7552  nqpru  7553  addnqprlemrl  7558  addnqprlemru  7559  prmuloc  7567  mulnqprlemrl  7574  mulnqprlemru  7575  ltsopr  7597  ltexprlemm  7601  ltexprlemopl  7602  ltexprlemopu  7604  lteupri  7618  recexprlemopl  7626  recexprlemopu  7628  recexprlemdisj  7631  archpr  7644  cauappcvgprlemdisj  7652  cauappcvgprlemladdrl  7658  cauappcvgprlem2  7661  caucvgprlemnbj  7668  caucvgprlemdisj  7675  caucvgprlemladdfu  7678  caucvgprlem2  7681  caucvgprprlemnbj  7694  caucvgprprlemdisj  7703  suplocexprlemml  7717  suplocexprlemrl  7718  suplocexprlemmu  7719  suplocexprlemloc  7722  addsrmo  7744  mulsrmo  7745  recexgt0sr  7774  prsrpos  7786  caucvgsrlemasr  7791  suplocsrlemb  7807  suplocsrlempr  7808  suplocsr  7810  elrealeu  7830  pitonn  7849  pitoregt0  7850  pitore  7851  recnnre  7852  axaddcl  7865  axaddrcl  7866  axmulcl  7867  axmulrcl  7868  axrnegex  7880  axcnre  7882  axpre-lttrn  7885  rereceu  7890  axarch  7892  axpre-suploclemres  7902  axpre-suploc  7903  ltxrlt  8025  apirr  8564  divmulasscomap  8655  rerecclap  8689  lbreu  8904  arch  9175  0mnnnnn0  9210  nnm1nn0  9219  elnnnn0c  9223  elnnz1  9278  ztri3or0  9297  nzadd  9307  nn0n0n1ge2  9325  zdceq  9330  zdcle  9331  zdclt  9332  uzind  9366  eluzge3nn  9574  supinfneg  9597  infsupneg  9598  eluz2b2  9605  elnn1uz2  9609  elnn0dc  9613  elnndc  9614  nn01to3  9619  znq  9626  qaddcl  9637  qmulcl  9639  qreccl  9644  irradd  9648  irrmul  9649  elpq  9650  cnref1o  9652  xnn0dcle  9804  xrpnfdc  9844  xrmnfdc  9845  xaddcom  9863  xnegdi  9870  xpncan  9873  xleadd1a  9875  iooidg  9911  elioo4g  9936  elfzd  10018  fzdcel  10042  fznlem  10043  fzpreddisj  10073  fz0to4untppr  10126  elfz0ubfz0  10127  elfz0fzfz0  10128  fz0fzelfz0  10129  fz0fzdiffz0  10132  elfzmlbp  10134  difelfzle  10136  4fvwrd4  10142  fzosplit  10179  elfzo0  10184  fzo1fzo0n0  10185  elfzonn0  10188  fzofzim  10190  elfzo1  10192  elfzom1elp1fzo  10204  fzossfzop1  10214  ssfzo12bi  10227  exfzdc  10242  qdceq  10249  exbtwnzlemstep  10250  exbtwnzlemex  10252  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2z  10257  qbtwnxr  10260  modfzo0difsn  10397  frec2uzrand  10407  frec2uzf1od  10408  frecuzrdgrcl  10412  frecuzrdgtcl  10414  frecuzrdgrclt  10417  frecuzrdgfunlem  10421  frecfzennn  10428  seq3f1olemp  10504  seq3f1oleml  10505  ser0f  10517  expcl2lemap  10534  hashunsng  10789  shftfvalg  10829  shftfval  10832  caucvgre  10992  rexanuz  10999  recvguniq  11006  rennim  11013  resqrexlemf  11018  rsqrmo  11038  fimaxre2  11237  climeu  11306  sumdc  11368  summodc  11393  zsumdc  11394  isum  11395  fisumss  11402  isumss2  11403  fsumsplit  11417  sumsnf  11419  fsumsplitsn  11420  sumtp  11424  sumsplitdc  11442  fsum2dlemstep  11444  fisum0diag2  11457  fsumconst  11464  modfsummodlemstep  11467  fsum00  11472  fsumabs  11475  fsumiun  11487  isumlessdc  11506  expcnv  11514  prodmodc  11588  zproddc  11589  iprodap  11590  iprodap0  11592  fprodssdc  11600  prodsnf  11602  fprodsplitdc  11606  fprodsplit  11607  fprodm1  11608  fprod1p  11609  fprodunsn  11614  fprod2dlemstep  11632  fprodsplitsn  11643  ef0lem  11670  modmulconst  11832  dvdsdivcl  11858  dvdsssfz1  11860  dvdsfac  11868  zeoxor  11876  nn0ehalf  11910  nn0oddm1d2  11916  nnoddm1d2  11917  divalglemeunn  11928  divalglemeuneg  11930  zsupcllemstep  11948  infssuzex  11952  gcdsupex  11960  gcdsupcl  11961  bezoutlemnewy  11999  bezoutlemmain  12001  bezoutlemeu  12010  dfgcd2  12017  nnwosdc  12042  algrf  12047  algcvgblem  12051  lcmgcdlem  12079  lcmdvds  12081  coprmgcdb  12090  mulgcddvds  12096  qredeu  12099  cncongr1  12105  cncongr2  12106  isprm2lem  12118  dvdsnprmd  12127  prmdc  12132  oddprmge3  12137  pw2dvdseu  12170  phibndlem  12218  dfphi2  12222  hashdvds  12223  phiprmpw  12224  eulerthlemh  12233  hashgcdeq  12241  phisum  12242  odzdvds  12247  reumodprminv  12255  nnnn0modprm0  12257  prm23ge5  12266  pclemdc  12290  pcdvdsb  12321  difsqpwdvds  12339  oddprmdvds  12354  1arith  12367  4sqlem3  12390  ennnfonelemdc  12402  ennnfonelemh  12407  ennnfonelemhf1o  12416  ennnfonelemf1  12421  ennnfonelemrn  12422  ennnfonelemdm  12423  exmidunben  12429  ctinfomlemom  12430  ctinfom  12431  ctiunctlemudc  12440  ctiunctlemf  12441  ctiunctal  12444  nninfdclemcl  12451  nninfdclemf  12452  nninfdclemp1  12453  isstructim  12478  setsresg  12502  strleund  12564  1strbas  12578  2strbasg  12580  2stropg  12581  restsspw  12703  tgval  12716  ptex  12718  imasaddfnlemg  12740  fnpr2o  12763  fnpr2ob  12764  mgmidsssn0  12808  isnsgrp  12817  sgrpidmndm  12826  mndinvmod  12851  mnd1  12852  mhmeql  12881  grpinveu  12916  mulgval  12991  subgintm  13063  trivsubgsnd  13066  eqgfval  13086  iscmnd  13106  srgfcl  13161  reldvdsrsrg  13266  subrgdvds  13361  lssuni  13455  lssintclm  13476  istopon  13552  toponcom  13566  topgele  13568  topontopn  13576  tsettps  13577  eltg2b  13593  unitg  13601  tgss2  13618  bastop2  13623  distop  13624  epttop  13629  cldss2  13645  neisspw  13687  neipsm  13693  neiuni  13700  tgcn  13747  tgcnp  13748  cnntr  13764  lmff  13788  txuni2  13795  txbasex  13796  txbas  13797  txcnp  13810  txcnmpt  13812  txcn  13814  txdis  13816  txdis1cn  13817  cnmpt11  13822  cnmpt12  13826  cnmpt21  13830  cnmpt2t  13832  cnmpt22  13833  blsscls2  14032  xmetxpbl  14047  xmettxlem  14048  tgqioo  14086  fsumcncntop  14095  cncfmpt1f  14123  mulcncflem  14129  mulcncf  14130  dedekindeu  14140  dedekindicclemicc  14149  dedekindicc  14150  ivthinclemdisj  14157  limcimo  14173  cnmptlimc  14182  reldvg  14187  dvfvalap  14189  dvfgg  14196  dveflem  14226  dvef  14227  sincn  14229  coscn  14230  reeff1o  14233  pilem3  14243  ioocosf1o  14314  lgsne0  14478  lgseisenlem2  14490  2sqlem2  14501  mul2sq  14502  2sqlem3  14503  2sqlem7  14507  bj-trst  14530  bj-fast  14532  bj-stand  14539  bj-trdc  14543  bj-fadc  14545  decidr  14587  djulclALT  14592  djurclALT  14593  bj-charfunr  14601  bj-indind  14723  bj-2inf  14729  bj-nntrans2  14743  bj-peano4  14746  bj-nnord  14749  bj-inf2vn  14765  bj-inf2vn2  14766  bj-findis  14770  pwf1oexmid  14788  subctctexmid  14789  nnsf  14793  nninfsellemdc  14798  nninffeq  14808  exmidsbthrlem  14809  sbthom  14813  triap  14816  trilpo  14830  apdifflemr  14834  redcwlpo  14842  tridceq  14843  nconstwlpolem0  14850  nconstwlpolem  14852  nconstwlpo  14853  neapmkv  14855  ltlenmkv  14857