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-1 5  ax-2 6  ax-mp 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  411  oibabs  686  dcim  809  dcstab  812  stdcndc  813  stdcndcOLD  814  dcor  900  3mix1  1131  3mix2  1132  3jca  1142  syl3anbrc  1146  inegd  1331  pclem6  1333  xoranor  1336  nfxfrd  1432  nfd  1484  hban  1507  nfan1  1524  nford  1527  nfand  1528  hbim1  1530  alexim  1605  ax6blem  1609  nf4r  1630  19.34  1643  nfexd  1715  sbcof2  1762  nfsb2or  1789  sbidm  1803  nfdv  1829  nfeudv  1988  mon  2002  eumo  2005  mo23  2014  eu2  2017  eu3h  2018  exmodc  2023  exmonim  2024  mo2r  2025  mo3h  2026  bm1.1  2098  eqrdv  2111  3eltr4g  2198  abbi2dv  2231  abbi1dv  2232  nfcd  2248  nfcxfrd  2251  dcned  2286  neqned  2287  3netr4g  2315  necon3bi  2330  necon2ai  2334  alral  2450  rspe  2453  rsp2e  2455  rgen2a  2458  ralrimi  2475  r19.27v  2531  r19.28v  2532  r19.27av  2539  r19.32r  2550  nfreudxy  2576  mormo  2614  nrexrmo  2619  cgsex2g  2691  cgsex4g  2692  spc2egv  2744  spc2gv  2745  spc3egv  2746  spc3gv  2747  rspce  2753  ceqex  2780  elrab3t  2806  elrabd  2809  mosubt  2828  mo2icl  2830  reu3  2841  reu6i  2842  2rmorex  2857  sbc5  2899  rspesbca  2959  rmo2ilem  2964  sbnfc2  3024  ssrd  3066  ssrdv  3067  3sstr4g  3104  syl5eqss  3107  ss2abdv  3134  abssdv  3135  rabssdv  3141  ss2rabdv  3142  ssun1  3203  unssad  3217  unssbd  3218  ssddif  3274  uneqin  3291  indifdir  3296  undif3ss  3301  reuss2  3320  n0rf  3339  reximdva0m  3342  rabxmdc  3358  ssindif0im  3386  minel  3388  ralidm  3427  ralm  3431  dcun  3437  ifmdc  3473  disjsn2  3550  absneu  3559  rabsneu  3560  opprc  3690  elunii  3705  dfnfc2  3718  uniss2  3731  unidif  3732  ssunieq  3733  intab  3764  iunss2  3822  iunxdif2  3825  invdisj  3887  disjiun  3888  3brtr4g  3925  trin  3994  triun  3997  truni  3998  trint  3999  iinexgm  4037  class2seteq  4045  pwuni  4074  exmid1dc  4081  exmidn0m  4082  exmidsssn  4083  exmid0el  4085  exmidel  4086  exmidundif  4087  exmidundifim  4088  mss  4106  copsex2t  4125  euotd  4134  pwunim  4166  ispod  4184  sotricim  4203  exse  4216  frind  4232  trssord  4260  suctr  4301  pwnex  4328  eusvnf  4332  eusvnfb  4333  eusv2nf  4335  rexxfrd  4342  ralxfr2d  4343  rexxfr2d  4344  rabxfrd  4348  reuhypd  4350  eldifpw  4356  iunpw  4359  ssorduni  4361  sucelon  4377  onsucelsucr  4382  sucunielr  4384  ordtri2or2exmidlem  4399  onsucelsucexmid  4403  reg2exmidlema  4407  setindel  4411  elirr  4414  orddisj  4419  en2lp  4427  suc11g  4430  ordsuc  4436  nlimsucg  4439  ordtri2or2exmid  4444  zfregfr  4446  wessep  4450  tfi  4454  peano5  4470  limom  4485  peano2b  4486  nndceq0  4489  nnpredcl  4494  0nelrel  4543  eqrelrdv  4593  xpsspw  4609  relint  4621  relop  4647  eqbrrdva  4667  opeldm  4700  elres  4811  relssres  4813  exse2  4869  issref  4877  trin2  4886  dminss  4909  imainss  4910  rnxpid  4929  dmsn0el  4964  dmmptg  4992  relrelss  5021  cnviinm  5036  iotanul  5059  sniota  5071  dffun5r  5091  funmo  5094  funco  5119  funun  5123  funprg  5129  funtpg  5130  funtp  5132  fntpg  5135  fununi  5147  funcnvuni  5148  imadiflem  5158  imainlem  5160  funimaexglem  5162  isarep2  5166  fnunsn  5186  2elresin  5190  fnimadisj  5199  dmmptd  5209  fco  5244  funssxp  5248  fssres  5254  feu  5261  fimacnvdisj  5263  fabexg  5266  f00  5270  f0rn0  5273  f1co  5296  fores  5310  foco  5311  f1ores  5336  foimacnv  5339  f1oun  5341  fun11iun  5342  f1oco  5344  fo00  5357  brprcneu  5366  fv3  5396  relelfvdm  5405  nfvres  5406  nfunsn  5407  funfvbrb  5485  respreima  5500  dff2  5516  dff3im  5517  dffo4  5520  fvmptelrn  5525  ffvresb  5535  f1oresrab  5537  fmptco  5538  fsn  5544  fpr  5554  ftpg  5556  fsnunf  5572  fsnunfv  5573  elabrex  5611  dff1o6  5629  foeqcnvco  5643  fliftel1  5647  isores1  5667  isoini2  5672  riotasbc  5697  acexmidlemph  5719  acexmidlemcase  5721  oprabidlem  5754  brabvv  5769  eloprabga  5810  fnoprabg  5824  caovimo  5916  oprabexd  5977  fo1stresm  6011  fo2ndresm  6012  unielxp  6024  1st2ndbr  6034  fmpoco  6065  1stconst  6070  2ndconst  6071  poxp  6081  spc2ed  6082  disjxp1  6085  reldmtpos  6102  tposfun  6109  dftpos4  6112  smores  6141  smores2  6143  tfrlem1  6157  tfr0dm  6171  tfrlemibxssdm  6176  tfrlemibex  6178  tfrlemiubacc  6179  tfrlemi14d  6182  tfrexlem  6183  tfri1d  6184  tfr1onlembxssdm  6192  tfr1onlembex  6194  tfr1onlemubacc  6195  tfr1onlemres  6198  tfrcllemsucfn  6202  tfrcllembxssdm  6205  tfrcllembex  6207  tfrcllemubacc  6208  tfrcllemres  6211  tfri3  6216  rdgon  6235  frecabcl  6248  frecfcllem  6253  frecrdg  6257  2oconcl  6288  nnsucelsuc  6339  nntri3or  6341  nndceq  6347  nndcel  6348  dcdifsnid  6352  ecexr  6386  brdifun  6408  ecelqsdm  6451  iinerm  6453  eroveu  6472  erovlem  6473  ecopovtrn  6478  ecopovtrng  6481  th3qlem1  6483  pmsspw  6529  map0b  6533  mapsn  6536  mapsncnv  6541  ixpf  6566  uniixp  6567  ixpexgg  6568  resixp  6579  f1oen3g  6600  ssdomg  6624  domtr  6631  snfig  6660  xpf1o  6689  xpmapenlem  6694  php5dom  6708  fidceq  6714  nnfi  6717  fiunsnnn  6726  findcard  6733  findcard2  6734  findcard2s  6735  ac6sfi  6743  tridc  6744  fimax2gtri  6746  finexdc  6747  exmidpw  6753  nnwetri  6755  unsnfi  6758  unsnfidcex  6759  unsnfidcel  6760  undifdcss  6762  tpfidisj  6767  iunfidisj  6784  snexxph  6788  fidcenumlemrks  6791  sbthlem2  6796  sbthlemi3  6797  sbthlem7  6801  sbthlemi8  6802  fival  6808  supmoti  6830  djuss  6905  updjudhf  6914  updjud  6917  casefun  6920  caseinj  6924  omp1eomlem  6929  djufun  6939  djuinj  6941  ctssdccl  6946  finomni  6960  exmidomniim  6961  exmidomni  6962  fodjuomnilemdc  6964  nnnninf  6971  exmidfodomrlemr  7003  exmidfodomrlemrALT  7004  exmidaclem  7009  dju1en  7014  dmaddpqlem  7127  nqpi  7128  dmaddpq  7129  dmmulpq  7130  ltdcnq  7147  subhalfnqq  7164  enq0sym  7182  enq0ref  7183  enq0tr  7184  nqnq0pi  7188  nq0nn  7192  addnq0mo  7197  mulnq0mo  7198  nqpnq0nq  7203  nqnq0a  7204  nqnq0m  7205  npsspw  7221  elnp1st2nd  7226  prnmaxl  7238  prnminu  7239  prarloc  7253  genprndl  7271  genprndu  7272  nqprm  7292  nqprl  7301  nqpru  7302  addnqprlemrl  7307  addnqprlemru  7308  prmuloc  7316  mulnqprlemrl  7323  mulnqprlemru  7324  ltsopr  7346  ltexprlemm  7350  ltexprlemopl  7351  ltexprlemopu  7353  lteupri  7367  recexprlemopl  7375  recexprlemopu  7377  recexprlemdisj  7380  archpr  7393  cauappcvgprlemdisj  7401  cauappcvgprlemladdrl  7407  cauappcvgprlem2  7410  caucvgprlemnbj  7417  caucvgprlemdisj  7424  caucvgprlemladdfu  7427  caucvgprlem2  7430  caucvgprprlemnbj  7443  caucvgprprlemdisj  7452  addsrmo  7480  mulsrmo  7481  recexgt0sr  7510  prsrpos  7521  caucvgsrlemasr  7526  elrealeu  7558  pitonn  7577  pitoregt0  7578  pitore  7579  recnnre  7580  axaddcl  7593  axaddrcl  7594  axmulcl  7595  axmulrcl  7596  axrnegex  7608  axcnre  7610  axpre-lttrn  7613  rereceu  7618  axarch  7620  ltxrlt  7748  apirr  8279  cnstab  8318  divmulasscomap  8363  rerecclap  8397  lbreu  8607  arch  8872  0mnnnnn0  8907  nnm1nn0  8916  elnnnn0c  8920  elnnz1  8975  ztri3or0  8994  nzadd  9004  nn0n0n1ge2  9019  zdceq  9024  zdcle  9025  zdclt  9026  uzind  9060  eluzge3nn  9263  supinfneg  9286  infsupneg  9287  eluz2b2  9293  elnn1uz2  9297  nn01to3  9305  znq  9312  qaddcl  9323  qmulcl  9325  qreccl  9330  irradd  9334  irrmul  9335  cnref1o  9336  xrpnfdc  9512  xrmnfdc  9513  xaddcom  9531  xnegdi  9538  xpncan  9541  xleadd1a  9543  iooidg  9579  elioo4g  9604  fzdcel  9707  fznlem  9708  fzpreddisj  9738  elfz0ubfz0  9789  elfz0fzfz0  9790  fz0fzelfz0  9791  fz0fzdiffz0  9794  elfzmlbp  9796  difelfzle  9798  4fvwrd4  9804  fzosplit  9841  elfzo0  9846  fzo1fzo0n0  9847  elfzonn0  9850  fzofzim  9852  elfzo1  9854  elfzom1elp1fzo  9866  fzossfzop1  9876  ssfzo12bi  9889  exfzdc  9904  qdceq  9911  exbtwnzlemstep  9912  exbtwnzlemex  9914  exbtwnz  9915  rebtwn2zlemstep  9917  rebtwn2z  9919  qbtwnxr  9922  modfzo0difsn  10055  frec2uzrand  10065  frec2uzf1od  10066  frecuzrdgrcl  10070  frecuzrdgtcl  10072  frecuzrdgrclt  10075  frecuzrdgfunlem  10079  frecfzennn  10086  seq3f1olemp  10162  seq3f1oleml  10163  ser0f  10175  expcl2lemap  10192  hashunsng  10440  shftfvalg  10477  shftfval  10480  caucvgre  10639  rexanuz  10646  recvguniq  10653  rennim  10660  resqrexlemf  10665  rsqrmo  10685  fimaxre2  10884  climeu  10951  sumdc  11013  summodc  11038  zsumdc  11039  isum  11040  fisumss  11047  isumss2  11048  fsumsplit  11062  sumsnf  11064  fsumsplitsn  11065  sumtp  11069  sumsplitdc  11087  fsum2dlemstep  11089  fisum0diag2  11102  fsumconst  11109  modfsummodlemstep  11112  fsum00  11117  fsumabs  11120  fsumiun  11132  isumlessdc  11151  expcnv  11159  ef0lem  11211  modmulconst  11367  dvdsdivcl  11390  dvdsssfz1  11392  dvdsfac  11400  zeoxor  11408  nn0ehalf  11442  nn0oddm1d2  11448  nnoddm1d2  11449  divalglemeunn  11460  divalglemeuneg  11462  zsupcllemstep  11480  infssuzex  11484  gcdsupex  11488  gcdsupcl  11489  bezoutlemnewy  11524  bezoutlemmain  11526  bezoutlemeu  11535  dfgcd2  11542  algrf  11566  algcvgblem  11570  lcmgcdlem  11598  lcmdvds  11600  coprmgcdb  11609  mulgcddvds  11615  qredeu  11618  cncongr1  11624  cncongr2  11625  isprm2lem  11637  dvdsnprmd  11646  oddprmge3  11655  pw2dvdseu  11685  phibndlem  11731  dfphi2  11735  hashdvds  11736  phiprmpw  11737  hashgcdeq  11743  ennnfonelemdc  11751  ennnfonelemh  11756  ennnfonelemhf1o  11765  ennnfonelemf1  11770  ennnfonelemrn  11771  ennnfonelemdm  11772  exmidunben  11778  ctinfomlemom  11779  ctinfom  11780  ctiunctlemudc  11787  ctiunctlemf  11788  isstructim  11810  setsresg  11834  strleund  11884  1strbas  11895  2strbasg  11897  2stropg  11898  restsspw  11967  istopon  12017  toponcom  12031  topgele  12033  topontopn  12041  tsettps  12042  tgval  12055  eltg2b  12060  unitg  12068  tgss2  12085  bastop2  12090  distop  12091  epttop  12096  cldss2  12112  neisspw  12154  neipsm  12160  neiuni  12167  tgcn  12213  tgcnp  12214  cnntr  12230  lmff  12254  txuni2  12261  txbasex  12262  txbas  12263  txcnp  12276  txcnmpt  12278  txcn  12280  txdis  12282  txdis1cn  12283  cnmpt11  12288  cnmpt12  12292  cnmpt21  12296  cnmpt2t  12298  cnmpt22  12299  blsscls2  12476  xmetxpbl  12491  xmettxlem  12492  tgqioo  12527  fsumcncntop  12536  cncfmpt1f  12564  mulcncflem  12570  mulcncf  12571  limcimo  12584  cnmptlimc  12593  reldvg  12597  dvfvalap  12599  dvfgg  12606  bj-nnal  12633  bj-trst  12634  bj-fast  12635  bj-stand  12639  bj-trdc  12641  bj-fadc  12642  decidr  12686  djulclALT  12691  djurclALT  12692  bj-indind  12813  bj-2inf  12819  bj-nntrans2  12833  bj-peano4  12836  bj-nnord  12839  bj-inf2vn  12855  bj-inf2vn2  12856  bj-findis  12860  pwf1oexmid  12877  nnsf  12880  nninfsellemdc  12887  nninffeq  12897  exmidsbthrlem  12898  sbthom  12902  triap  12905  trilpo  12917