Theorem sylibr 133

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 132	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbbr  135  pm5.74rd  182  bitri  183  3imtr4i  200  sylanbrc  414  oibabs  704  dcim  827  dcstab  830  stdcndc  831  stdcndcOLD  832  dcor  920  3mix1  1151  3mix2  1152  3jca  1162  syl3anbrc  1166  inegd  1354  pclem6  1356  xoranor  1359  nfxfrd  1455  nfd  1503  hban  1527  nfan1  1544  nford  1547  nfand  1548  hbim1  1550  nfal  1556  alexim  1625  nnal  1629  ax6blem  1630  nf4r  1651  19.34  1664  nfexd  1741  sbcof2  1790  nfsb2or  1817  sbidm  1831  nfdv  1857  nfd2  2002  nfeudv  2021  mon  2035  eumo  2038  mo23  2047  eu2  2050  eu3h  2051  exmodc  2056  exmonim  2057  mo2r  2058  mo3h  2059  bm1.1  2142  eqrdv  2155  3eltr4g  2243  abbi2dv  2276  abbi1dv  2277  nfcd  2294  nfcxfrd  2297  dcned  2333  neqned  2334  3netr4g  2362  necon3bi  2377  necon2ai  2381  nnral  2447  alral  2502  rspe  2506  rsp2e  2508  rgen2a  2511  ralrimi  2528  r19.27v  2584  r19.28v  2585  r19.27av  2592  r19.32r  2603  nfreudxy  2630  mormo  2668  nrexrmo  2673  cgsex2g  2748  cgsex4g  2749  spc2egv  2802  spc2gv  2803  spc3egv  2804  spc3gv  2805  rspce  2811  ceqex  2839  elrab3t  2867  elrabd  2870  mosubt  2889  mo2icl  2891  reu3  2902  reu6i  2903  2rmorex  2918  sbc5  2960  rspesbca  3021  rmo2ilem  3026  sbnfc2  3091  ssrd  3133  ssrdv  3134  3sstr4g  3171  eqsstrid  3174  ss2abdv  3201  abssdv  3202  rabssdv  3208  ss2rabdv  3209  ssun1  3271  unssad  3285  unssbd  3286  ssddif  3342  uneqin  3359  indifdir  3364  undif3ss  3369  reuss2  3388  n0rf  3407  reximdva0m  3410  rabxmdc  3426  ssindif0im  3454  minel  3456  ralidm  3495  ralm  3499  dcun  3505  ifmdc  3543  disjsn2  3624  absneu  3633  rabsneu  3634  opprc  3764  elunii  3779  dfnfc2  3792  uniss2  3805  unidif  3806  ssunieq  3807  intab  3838  iunss2  3896  iunxdif2  3899  invdisj  3961  disjiun  3962  3brtr4g  4000  trin  4074  triun  4077  truni  4078  trint  4079  iinexgm  4117  class2seteq  4126  pwuni  4155  exmid1dc  4163  exmidn0m  4164  exmidsssn  4165  exmid0el  4167  exmidel  4168  exmidundif  4169  exmidundifim  4170  mss  4188  copsex2t  4207  euotd  4216  pwunim  4248  ispod  4266  sotricim  4285  exse  4298  frind  4314  trssord  4342  suctr  4383  pwnex  4411  eusvnf  4415  eusvnfb  4416  eusv2nf  4418  rexxfrd  4425  ralxfr2d  4426  rexxfr2d  4427  rabxfrd  4431  reuhypd  4433  eldifpw  4439  iunpw  4442  ssorduni  4448  sucelon  4464  onsucelsucr  4469  sucunielr  4471  ontriexmidim  4483  ordtri2or2exmidlem  4487  onsucelsucexmid  4491  reg2exmidlema  4495  setindel  4499  elirr  4502  orddisj  4507  en2lp  4515  suc11g  4518  ordsuc  4524  nlimsucg  4527  ordtri2or2exmid  4532  ontri2orexmidim  4533  zfregfr  4535  wessep  4539  tfi  4543  peano5  4559  limom  4575  peano2b  4576  nndceq0  4579  nnpredcl  4584  0nelrel  4634  eqrelrdv  4684  xpsspw  4700  relint  4712  relop  4738  eqbrrdva  4758  opeldm  4791  elres  4904  relssres  4906  exse2  4962  issref  4970  trin2  4979  dminss  5002  imainss  5003  rnxpid  5022  dmsn0el  5057  dmmptg  5085  relrelss  5114  cnviinm  5129  iotanul  5152  sniota  5164  dffun5r  5184  funmo  5187  funco  5212  funun  5216  funprg  5222  funtpg  5223  funtp  5225  fntpg  5228  fununi  5240  funcnvuni  5241  imadiflem  5251  imainlem  5253  funimaexglem  5255  isarep2  5259  fnunsn  5279  2elresin  5283  fnimadisj  5292  dmmptd  5302  fco  5337  funssxp  5341  fssres  5347  feu  5354  fimacnvdisj  5356  fabexg  5359  f00  5363  f0rn0  5366  f1co  5389  fores  5403  foco  5404  f1ores  5431  foimacnv  5434  f1oun  5436  fun11iun  5437  f1oco  5439  fo00  5452  brprcneu  5463  fv3  5493  relelfvdm  5502  nfvres  5503  nfunsn  5504  funfvbrb  5582  respreima  5597  dff2  5613  dff3im  5614  dffo4  5617  fvmptelrn  5622  ffvresb  5632  f1oresrab  5634  fmptco  5635  fsn  5641  fpr  5651  ftpg  5653  fsnunf  5669  fsnunfv  5670  elabrex  5710  dff1o6  5728  foeqcnvco  5742  fliftel1  5746  isores1  5766  isoini2  5771  riotasbc  5797  acexmidlemph  5819  acexmidlemcase  5821  oprabidlem  5854  brabvv  5869  eloprabga  5910  fnoprabg  5924  caovimo  6016  oprabexd  6077  fo1stresm  6111  fo2ndresm  6112  unielxp  6124  1st2ndbr  6134  fmpoco  6165  1stconst  6170  2ndconst  6171  poxp  6181  spc2ed  6182  disjxp1  6185  reldmtpos  6202  tposfun  6209  dftpos4  6212  smores  6241  smores2  6243  tfrlem1  6257  tfr0dm  6271  tfrlemibxssdm  6276  tfrlemibex  6278  tfrlemiubacc  6279  tfrlemi14d  6282  tfrexlem  6283  tfri1d  6284  tfr1onlembxssdm  6292  tfr1onlembex  6294  tfr1onlemubacc  6295  tfr1onlemres  6298  tfrcllemsucfn  6302  tfrcllembxssdm  6305  tfrcllembex  6307  tfrcllemubacc  6308  tfrcllemres  6311  tfri3  6316  rdgon  6335  frecabcl  6348  frecfcllem  6353  frecrdg  6357  2oconcl  6388  nnsucelsuc  6440  nntri3or  6442  nndceq  6448  nndcel  6449  dcdifsnid  6453  ecexr  6487  brdifun  6509  ecelqsdm  6552  iinerm  6554  eroveu  6573  erovlem  6574  ecopovtrn  6579  ecopovtrng  6582  th3qlem1  6584  pmsspw  6630  map0b  6634  mapsn  6637  mapsncnv  6642  ixpf  6667  uniixp  6668  ixpexgg  6669  resixp  6680  f1oen3g  6701  ssdomg  6725  domtr  6732  snfig  6761  enpr2d  6764  xpf1o  6791  xpmapenlem  6796  php5dom  6810  fidceq  6816  nnfi  6819  fiunsnnn  6828  findcard  6835  findcard2  6836  findcard2s  6837  ac6sfi  6845  tridc  6846  fimax2gtri  6848  finexdc  6849  exmidpw  6855  exmidpweq  6856  nnwetri  6862  unsnfi  6865  unsnfidcex  6866  unsnfidcel  6867  undifdcss  6869  tpfidisj  6874  iunfidisj  6892  snexxph  6896  fidcenumlemrks  6899  sbthlem2  6904  sbthlemi3  6905  sbthlem7  6909  sbthlemi8  6910  fival  6916  dcfi  6927  supmoti  6939  djuss  7016  updjudhf  7025  updjud  7028  casefun  7031  caseinj  7035  omp1eomlem  7040  djufun  7050  djuinj  7052  ctssdccl  7057  ctfoex  7064  nnnninf  7071  nnnninfeq2  7074  nninfisollem0  7075  nninfisollemne  7076  nninfisollemeq  7077  nninfisol  7078  finomni  7085  exmidomniim  7086  exmidomni  7087  fodjuomnilemdc  7089  omniwomnimkv  7112  exmidonfinlem  7130  exmidfodomrlemr  7139  exmidfodomrlemrALT  7140  exmidaclem  7145  dju1en  7150  exmidontriimlem1  7158  exmidontriimlem3  7160  pw1on  7163  3nsssucpw1  7173  cc4f  7191  cc4n  7193  dmaddpqlem  7299  nqpi  7300  dmaddpq  7301  dmmulpq  7302  ltdcnq  7319  subhalfnqq  7336  enq0sym  7354  enq0ref  7355  enq0tr  7356  nqnq0pi  7360  nq0nn  7364  addnq0mo  7369  mulnq0mo  7370  nqpnq0nq  7375  nqnq0a  7376  nqnq0m  7377  npsspw  7393  elnp1st2nd  7398  prnmaxl  7410  prnminu  7411  prarloc  7425  genprndl  7443  genprndu  7444  nqprm  7464  nqprl  7473  nqpru  7474  addnqprlemrl  7479  addnqprlemru  7480  prmuloc  7488  mulnqprlemrl  7495  mulnqprlemru  7496  ltsopr  7518  ltexprlemm  7522  ltexprlemopl  7523  ltexprlemopu  7525  lteupri  7539  recexprlemopl  7547  recexprlemopu  7549  recexprlemdisj  7552  archpr  7565  cauappcvgprlemdisj  7573  cauappcvgprlemladdrl  7579  cauappcvgprlem2  7582  caucvgprlemnbj  7589  caucvgprlemdisj  7596  caucvgprlemladdfu  7599  caucvgprlem2  7602  caucvgprprlemnbj  7615  caucvgprprlemdisj  7624  suplocexprlemml  7638  suplocexprlemrl  7639  suplocexprlemmu  7640  suplocexprlemloc  7643  addsrmo  7665  mulsrmo  7666  recexgt0sr  7695  prsrpos  7707  caucvgsrlemasr  7712  suplocsrlemb  7728  suplocsrlempr  7729  suplocsr  7731  elrealeu  7751  pitonn  7770  pitoregt0  7771  pitore  7772  recnnre  7773  axaddcl  7786  axaddrcl  7787  axmulcl  7788  axmulrcl  7789  axrnegex  7801  axcnre  7803  axpre-lttrn  7806  rereceu  7811  axarch  7813  axpre-suploclemres  7823  axpre-suploc  7824  ltxrlt  7945  apirr  8484  divmulasscomap  8573  rerecclap  8607  lbreu  8821  arch  9092  0mnnnnn0  9127  nnm1nn0  9136  elnnnn0c  9140  elnnz1  9195  ztri3or0  9214  nzadd  9224  nn0n0n1ge2  9239  zdceq  9244  zdcle  9245  zdclt  9246  uzind  9280  eluzge3nn  9488  supinfneg  9511  infsupneg  9512  eluz2b2  9519  elnn1uz2  9523  elnn0dc  9527  nn01to3  9532  znq  9539  qaddcl  9550  qmulcl  9552  qreccl  9557  irradd  9561  irrmul  9562  elpq  9563  cnref1o  9565  xrpnfdc  9752  xrmnfdc  9753  xaddcom  9771  xnegdi  9778  xpncan  9781  xleadd1a  9783  iooidg  9819  elioo4g  9844  fzdcel  9948  fznlem  9949  fzpreddisj  9979  fz0to4untppr  10032  elfz0ubfz0  10033  elfz0fzfz0  10034  fz0fzelfz0  10035  fz0fzdiffz0  10038  elfzmlbp  10040  difelfzle  10042  4fvwrd4  10048  fzosplit  10085  elfzo0  10090  fzo1fzo0n0  10091  elfzonn0  10094  fzofzim  10096  elfzo1  10098  elfzom1elp1fzo  10110  fzossfzop1  10120  ssfzo12bi  10133  exfzdc  10148  qdceq  10155  exbtwnzlemstep  10156  exbtwnzlemex  10158  exbtwnz  10159  rebtwn2zlemstep  10161  rebtwn2z  10163  qbtwnxr  10166  modfzo0difsn  10303  frec2uzrand  10313  frec2uzf1od  10314  frecuzrdgrcl  10318  frecuzrdgtcl  10320  frecuzrdgrclt  10323  frecuzrdgfunlem  10327  frecfzennn  10334  seq3f1olemp  10410  seq3f1oleml  10411  ser0f  10423  expcl2lemap  10440  hashunsng  10692  shftfvalg  10729  shftfval  10732  caucvgre  10892  rexanuz  10899  recvguniq  10906  rennim  10913  resqrexlemf  10918  rsqrmo  10938  fimaxre2  11137  climeu  11204  sumdc  11266  summodc  11291  zsumdc  11292  isum  11293  fisumss  11300  isumss2  11301  fsumsplit  11315  sumsnf  11317  fsumsplitsn  11318  sumtp  11322  sumsplitdc  11340  fsum2dlemstep  11342  fisum0diag2  11355  fsumconst  11362  modfsummodlemstep  11365  fsum00  11370  fsumabs  11373  fsumiun  11385  isumlessdc  11404  expcnv  11412  prodmodc  11486  zproddc  11487  iprodap  11488  iprodap0  11490  fprodssdc  11498  prodsnf  11500  fprodsplitdc  11504  fprodsplit  11505  fprodm1  11506  fprod1p  11507  fprodunsn  11512  fprod2dlemstep  11530  fprodsplitsn  11541  ef0lem  11568  modmulconst  11730  dvdsdivcl  11754  dvdsssfz1  11756  dvdsfac  11764  zeoxor  11772  nn0ehalf  11806  nn0oddm1d2  11812  nnoddm1d2  11813  divalglemeunn  11824  divalglemeuneg  11826  zsupcllemstep  11844  infssuzex  11848  gcdsupex  11856  gcdsupcl  11857  bezoutlemnewy  11895  bezoutlemmain  11897  bezoutlemeu  11906  dfgcd2  11913  algrf  11937  algcvgblem  11941  lcmgcdlem  11969  lcmdvds  11971  coprmgcdb  11980  mulgcddvds  11986  qredeu  11989  cncongr1  11995  cncongr2  11996  isprm2lem  12008  dvdsnprmd  12017  prmdc  12022  oddprmge3  12027  pw2dvdseu  12058  phibndlem  12106  dfphi2  12110  hashdvds  12111  phiprmpw  12112  eulerthlemh  12121  hashgcdeq  12129  phisum  12130  odzdvds  12135  reumodprminv  12143  nnnn0modprm0  12145  prm23ge5  12154  pclemdc  12178  ennnfonelemdc  12198  ennnfonelemh  12203  ennnfonelemhf1o  12212  ennnfonelemf1  12217  ennnfonelemrn  12218  ennnfonelemdm  12219  exmidunben  12225  ctinfomlemom  12226  ctinfom  12227  ctiunctlemudc  12236  ctiunctlemf  12237  ctiunctal  12240  nninfdclemcl  12249  nninfdclemf  12250  nninfdclemp1  12251  isstructim  12274  setsresg  12298  strleund  12348  1strbas  12359  2strbasg  12361  2stropg  12362  restsspw  12431  istopon  12481  toponcom  12495  topgele  12497  topontopn  12505  tsettps  12506  tgval  12519  eltg2b  12524  unitg  12532  tgss2  12549  bastop2  12554  distop  12555  epttop  12560  cldss2  12576  neisspw  12618  neipsm  12624  neiuni  12631  tgcn  12678  tgcnp  12679  cnntr  12695  lmff  12719  txuni2  12726  txbasex  12727  txbas  12728  txcnp  12741  txcnmpt  12743  txcn  12745  txdis  12747  txdis1cn  12748  cnmpt11  12753  cnmpt12  12757  cnmpt21  12761  cnmpt2t  12763  cnmpt22  12764  blsscls2  12963  xmetxpbl  12978  xmettxlem  12979  tgqioo  13017  fsumcncntop  13026  cncfmpt1f  13054  mulcncflem  13060  mulcncf  13061  dedekindeu  13071  dedekindicclemicc  13080  dedekindicc  13081  ivthinclemdisj  13088  limcimo  13104  cnmptlimc  13113  reldvg  13118  dvfvalap  13120  dvfgg  13127  dveflem  13157  dvef  13158  sincn  13160  coscn  13161  reeff1o  13164  pilem3  13174  ioocosf1o  13245  bj-trst  13385  bj-fast  13387  bj-stand  13392  bj-trdc  13395  bj-fadc  13397  decidr  13441  djulclALT  13446  djurclALT  13447  bj-charfunr  13456  bj-indind  13578  bj-2inf  13584  bj-nntrans2  13598  bj-peano4  13601  bj-nnord  13604  bj-inf2vn  13620  bj-inf2vn2  13621  bj-findis  13625  pwf1oexmid  13642  exmid1stab  13643  subctctexmid  13644  nnsf  13648  nninfsellemdc  13653  nninffeq  13663  exmidsbthrlem  13664  sbthom  13668  triap  13671  trilpo  13685  apdifflemr  13689  redcwlpo  13697  tridceq  13698  nconstwlpolem0  13704  nconstwlpolem  13706  nconstwlpo  13707  neapmkv  13709